-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocRing 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₂ : NonUnitalNonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨_, ⟨⟩⟩

Result:
case mk.mk
R : Type u
inst₂ : NonUnitalNonAssocRing R
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝ right_distrib✝ zero_mul✝ mul_zero✝ = inst₂

Proof state:
case mk.mk.mk.mk
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝¹ right_distrib✝¹ zero_mul✝¹ mul_zero✝¹ = mk left_distrib✝ right_distrib✝ zero_mul✝ mul_zero✝

Tactic:
congr

Result:
case mk.mk.mk.mk.e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommGroup✝¹ = toAddCommGroup✝

Proof state:
case mk.mk.mk.mk.e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommGroup✝¹ = toAddCommGroup✝

Tactic:
ext : 1

Result:
case mk.mk.mk.mk.e_toAddCommGroup.h_mul
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ Add.add = Add.add

Proof state:
case mk.mk
R : Type u
inst₂ : NonUnitalNonAssocRing R
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝ right_distrib✝ zero_mul✝ mul_zero✝ = inst₂

Tactic:
rcases inst₂ with @⟨_, ⟨⟩⟩

Result:
case mk.mk.mk.mk
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝¹ right_distrib✝¹ zero_mul✝¹ mul_zero✝¹ = mk left_distrib✝ right_distrib✝ zero_mul✝ mul_zero✝

Proof state:
case mk.mk.mk.mk.e_toAddCommGroup.h_mul
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ Add.add = Add.add

Tactic:
assumption

Result:
no goals

Proof state:
case mk.mk.mk.mk.e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommGroup✝¹ = toAddCommGroup✝

Tactic:
(ext : 1; assumption)

Result:
no goals