-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : NonAssocSemiring R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁ = inst₂

Tactic:
have h_one' : (inst₁.toMulZeroOneClass).toMulOneClass.toOne
              = (inst₂.toMulZeroOneClass).toMulOneClass.toOne :=
  congrArg (@MulOneClass.toOne R) <| by ext : 1; exact h_mul

Result:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
⊢ inst₁ = inst₂

Proof state:
case a
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ Mul.mul = Mul.mul

Tactic:
exact h_mul

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
⊢ inst₁ = inst₂

Tactic:
have h_one : (inst₁.toMulZeroOneClass).toMulOneClass.toOne.one
             = (inst₂.toMulZeroOneClass).toMulOneClass.toOne.one :=
  congrArg (@One.one R) h_one'

Result:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ MulZeroOneClass.toMulOneClass = MulZeroOneClass.toMulOneClass

Tactic:
ext : 1

Result:
case a
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ Mul.mul = Mul.mul

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring

Tactic:
ext : 1 <;> assumption

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
⊢ toAddCommMonoidWithOne = toAddCommMonoidWithOne

Tactic:
ext : 1 <;> assumption

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ inst₁ = inst₂

Tactic:
have h_zero : (inst₁.toMulZeroClass).toZero.zero = (inst₂.toMulZeroClass).toZero.zero :=
  congrArg (fun inst => (inst.toMulZeroClass).toZero.zero) h

Result:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
this✝ : toAddCommMonoidWithOne = toAddCommMonoidWithOne
this : toNatCast = toNatCast
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Result:
case mk
R : Type u
inst₂ : NonAssocSemiring R
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
this✝ : toAddCommMonoidWithOne = toAddCommMonoidWithOne
this : toNatCast = toNatCast
⊢ mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
have : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne := by
  ext : 1 <;> assumption

Result:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
this : toAddCommMonoidWithOne = toAddCommMonoidWithOne
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring := by
  ext : 1 <;> assumption

Result:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ inst₁ = inst₂

Proof state:
case mk.mk
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
this✝ : toAddCommMonoidWithOne = toAddCommMonoidWithOne
this : toNatCast = toNatCast
⊢ mk one_mul✝¹ mul_one✝¹ natCast_zero✝¹ natCast_succ✝¹ = mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝

Tactic:
congr

Result:
no goals