example (α : Type) [Foo α] : α = Nat := by
induction α using Foo.induction_no with
| nat => rfl
example (α : Type) [Foo α] : α = Nat := by
induction α, ‹Foo α› using Foo.induction_ok with
| nat => rfl
**Expected behavior:** Both inductions should succeed
**Actual behavior:** The first one fails with "failed to infer implicit target ohno". It should be synthesizing the target via typeclass search, since it is in square brackets.
### Versions
* 4.8.0-rc1
* 4.9.0-nightly-2024-05-21
### Additional Information
[Additional information, configuration or data that might be necessary to reproduce the issue]
### Impact
Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others are impacted by this issue, please ask them to add :+1: to it.
@eric-wieser or others: could you say more about the (positive) impact of fixing this bug? Has it come up more often than with the single theorem mentioned on Zulip?
Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
The
induction
tactic does not handle instance-implicit arguments, as it treats them as regular implicits.Context
Zulip thread
Steps to Reproduce
instance : Foo Nat where
@[elab_as_elim] def Foo.induction_no (P : ∀ (α : Type) [Foo α], Prop) (nat : P Nat) (α : Type) [ohno : Foo α] : P α := sorry @[elab_as_elim] def Foo.induction_ok (P : ∀ (α : Type) [Foo α], Prop) (nat : P Nat) (α : Type) (ohok : Foo α) : P α := sorry
example (α : Type) [Foo α] : α = Nat := by induction α using Foo.induction_no with | nat => rfl
example (α : Type) [Foo α] : α = Nat := by induction α, ‹Foo α› using Foo.induction_ok with | nat => rfl