congr

Stream: lean4

[Scott Morrison]

The Lean3 analogue of this would have worked:

import Std.Tactic.RCases

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

/-- Typeclass for expressing that a type `M` with multiplication and a one satisfies
`1 * a = a` and `a * 1 = a` for all `a : M`. -/
class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂ := by
  rintro ⟨⟨one₁⟩, ⟨mul₁⟩, one_mul₁, mul_one₁⟩ ⟨⟨one₂⟩, ⟨mul₂⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩
  congr -- Does nothing!
  -- So this fails:
  exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

Any tips for getting similar behaviour in Lean4?

[Leonardo de Moura]

@Scott Morrison Could you please create a #mwe without imports and add an issue? Thanks.

[Scott Morrison]

I was worried you wouldn't like the rintro. :-) I'll work out how to fake it.

[Scott Morrison]

https://github.com/leanprover/lean4/issues/1711