Inductors and @[ext] with inaccessible implicits

Stream: mathlib4

[Robert Maxton]

Working on the equivalence of FreeProduct and PiTensorProduct when the algebras are all commutative. Have decided to write some ergonomics API for RingQuot, and wrote the following:

/--To prove a statement on an `x : RingQuot r`, it suffices to show that it can be
proven for all `a` with `x = mkAlgHom S r a`.-/
@[elab_as_elim, induction_eliminator, cases_eliminator]
theorem _root_.RingQuot.induction' {S A : Type*} [CommSemiring S] [Semiring A] [Algebra S A]
    {r : A → A → Prop} {motive : RingQuot r → Prop} (x : RingQuot r)
    (base : ∀ a : A, motive (RingQuot.mkAlgHom S r a)) : motive x := by
  obtain ⟨a, rfl⟩ := RingQuot.mkAlgHom_surjective S r x
  exact base a

/--To show that two `RingQuot r`s are equal, it suffices to show that they are the images
under `mkAlgHom` of some `s₁, s₂ ∈ S` related by `r`.-/
@[ext]
lemma _root_.RingQuot.ext_algHom {S A : Type*} [CommSemiring S] [Semiring A] [Algebra S A]
    {r : A → A → Prop}  {r₁ r₂ : RingQuot r}
    (h : ∀ {a₁ a₂}, r₁ = RingQuot.mkAlgHom S r a₁ → r₂ = RingQuot.mkAlgHom S r a₂ → r a₁ a₂) :
    -- {a₁ a₂ : A}
    -- (h₁ : r₁ = RingQuot.mkAlgHom S r a₁) (h₂ : r₂ = RingQuot.mkAlgHom S r a₂) (h : r a₁ a₂) :
    r₁ = r₂ := by
  cases r₁ with
  | base s₁ => _ /-dependent elimination failed, failed to solve equation
                   r₁ = (RingQuot.mkAlgHom ?m.455397 r) s₁-/
  rw [h₁, h₂, RingQuot.mkAlgHom_rel S h]

But, it doesn't work, because I haven't given it enough information to make it work: the ring S and its accompanying instances aren't determined by the motive I've given it.

[Robert Maxton]

In this case, I'm probably best served (for a number of reasons) by just retreating to RingQuot.mkRingHom instead. But in general, and if I wanted to make this specific case work for some reason, what would be the best approach?

[Robert Maxton]

For a match statement, I would probably try and fix this by adding an inaccessible match pattern | .(_), base s1 and matching on S as well. But a) I'm not sure that even works with induction_eliminator, and b) even if it does I'm pretty sure I'd have to make motive quantify over S to make that work, which means it'd take a bunch of type classes after S, which means that any use of that induction eliminator would probably involve a lot of _s to skip unwanted instances.

[Robert Maxton]

... Actually, now that I think about it, I should probably try just making the ring argument explicit and everything in between the usual instance-implicit

[Robert Maxton]

Hmmm, nope:

/--To prove a statement on an `x : RingQuot r`, it suffices to show that it can be
proven for any `mkAlgHom S r a`, `a : A`.-/
@[elab_as_elim, induction_eliminator, cases_eliminator]
theorem _root_.RingQuot.induction'
    {S A : Type*} [CommSemiring S] [Semiring A] [Algebra S A] {r : A → A → Prop}
    {motive : ∀ (S' : Type _) [CommSemiring S'] [Algebra S' A], RingQuot r → Prop}
    (x : RingQuot r)
    (base : ∀ (S' : Type _) [CommSemiring S'] [Algebra S' A] (a : A),
      motive S' (RingQuot.mkAlgHom S' r a)) : motive S x := by
  obtain ⟨a, rfl⟩ := RingQuot.mkAlgHom_surjective S r x
  exact base S a

/--To show that two `RingQuot r`s are equal, it suffices to show that they are the images
under `mkAlgHom` of some `s₁, s₂ ∈ S` related by `r`.-/
@[ext]
lemma _root_.RingQuot.ext_algHom {S A : Type*} [CommSemiring S] [Semiring A] [Algebra S A]
    {r : A → A → Prop}  {r₁ r₂ : RingQuot r}
    (h : ∀ {a₁ a₂}, r₁ = RingQuot.mkAlgHom S r a₁ → r₂ = RingQuot.mkAlgHom S r a₂ → r a₁ a₂) :
    r₁ = r₂ := by
  cases S, r₁ using RingQuot.induction' with
  | base S' s₁ => _ /-target
                        S
                      has type
                        Type u_5 : Type (u_5 + 1)
                      but is expected to have type
                        RingQuot ?m.451674 : Type ?u.451654-/

[Kyle Miller]

Maybe instead of using cases, try using refine directly here?

In the next Lean release, I think you'll be able to supply S to the using clause, if not already. It used to only accept an identifier, but it's been changed by @Joachim Breitner to accept a term.

[Robert Maxton]

Oh sure, I can use refine here. But I want the cases match syntax because while RingQuot has only one case, if you have multiple cases refine becomes much less convenient.

Supplying a ring to the using clause, huh. I'll try that next.