awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
⊢ Eq (α := (a : R) → S) (⇑(↑f : R →ₙ+* S) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_7
S : Type u_8
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
rw rw₁ : Eq (α := R →ₙ+* S) (↑g : R →ₙ+* S) (↑g : R →ₙ+* S)
⊢ Eq (α := R →ₙ+* S) (↑f : R →ₙ+* S) (↑g : R →ₙ+* S)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonUnitalNonAssocSemiring R
⊢ Eq (α := R →ₙ+* R) (toNonUnitalRingHom (refl R)) (NonUnitalRingHom.id R)

Tactic:
rfl

Premises used: RingEquiv.toNonUnitalRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ ∀ (y : S), (e.toNonUnitalRingHom : (a : R) → S) ((e.symm.toNonUnitalRingHom : (a : S) → R) y : R) = y

Tactic:
e.toEquiv.apply_symm_apply

Premises used: RingEquiv.toEquiv, Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ ∀ (x : R), (e.symm.toNonUnitalRingHom : (a : S) → R) ((e.toNonUnitalRingHom : (a : R) → S) x : S) = x

Tactic:
Equiv.symm_apply_apply e.toEquiv

Premises used: RingEquiv.toEquiv, Equiv.symm_apply_apply
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ (e₁.trans e₂).toNonUnitalRingHom = e₂.toNonUnitalRingHom.comp e₁.toNonUnitalRingHom

Tactic:
rfl

Premises used: RingEquiv.toNonUnitalRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
a :
  ∀ (x : S),
    Eq (α := S) ((e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom : (a : S) → S) x : S)
      ((NonUnitalRingHom.id S : (a : S) → S) x : S)
⊢ e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
x : S
⊢ Eq (α := S) ((e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom : (a : S) → S) x : S)
    ((NonUnitalRingHom.id S : (a : S) → S) x : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
a :
  ∀ (x : R),
    Eq (α := R) ((e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom : (a : R) → R) x : R)
      ((NonUnitalRingHom.id R : (a : R) → R) x : R)
⊢ e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
x : R
⊢ Eq (α := R) ((e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom : (a : R) → R) x : R)
    ((NonUnitalRingHom.id R : (a : R) → R) x : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Function.Injective (α := R ≃+* S) toRingHom

Tactic:
fun _ _ h =>
  RingEquiv.ext (RingHom.ext_iff.1 h)

Premises used: RingHom.ext_iff, RingEquiv.ext, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
⊢ f.toRingHom = (↑f : R →+* S)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, RingHomClass.toRingHom, RingEquiv.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
⊢ Eq (α := (a : R) → S) (⇑(↑f : R →+* S) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_7
S : Type u_8
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f g : R ≃+* S
h : f = g
rw rw₁ : Eq (α := R →+* S) (↑g : R →+* S) (↑g : R →+* S)
⊢ Eq (α := R →+* S) (↑f : R →+* S) (↑g : R →+* S)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
⊢ Eq (α := R →ₙ+* S) (↑(↑f : R →+* S) : R →ₙ+* S) (↑f : R →ₙ+* S)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, RingHomClass.toRingHom, NonUnitalRingHomClass.toNonUnitalRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
⊢ Eq (α := R →+ S) (RingHom.toAddMonoidHom (↑f : R →+* S)) (AddEquiv.toAddMonoidHom (↑f : R ≃+ S))

Tactic:
rfl

Premises used: AddEquiv.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
⊢ Eq (α := R →* S) (↑(↑f : R →+* S) : R →* S) (MulEquiv.toMonoidHom (↑f : R ≃* S))

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
⊢ AddEquiv.toEquiv (↑f : R ≃+ S) = MulEquiv.toEquiv (↑f : R ≃* S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonAssocSemiring R
⊢ Eq (α := R →+* R) (toRingHom (refl R)) (RingHom.id R)

Tactic:
rfl

Premises used: MulEquiv.toMonoidHom, RingEquiv.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonAssocSemiring R
⊢ Eq (α := R →* R) (toMonoidHom (refl R)) (MonoidHom.id R)

Tactic:
rfl

Premises used: MulEquiv.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonAssocSemiring R
⊢ Eq (α := R →+ R) (toAddMonoidHom (refl R)) (AddMonoidHom.id R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
⊢ ∀ (y : S), (e.toRingHom : (a : R) → S) ((e.symm.toRingHom : (a : S) → R) y : R) = y

Tactic:
e.toEquiv.apply_symm_apply

Premises used: RingEquiv.toEquiv, Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
⊢ ∀ (x : R), (e.symm.toRingHom : (a : S) → R) ((e.toRingHom : (a : R) → S) x : S) = x

Tactic:
Equiv.symm_apply_apply e.toEquiv

Premises used: RingEquiv.toEquiv, Equiv.symm_apply_apply
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ (e₁.trans e₂).toRingHom = e₂.toRingHom.comp e₁.toRingHom

Tactic:
rfl

Premises used: MulEquiv.toMonoidHom, RingEquiv.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
⊢ e.toRingHom.comp e.symm.toRingHom = RingHom.id S

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toRingHom.comp e.toRingHom = RingHom.id R

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
a : R
⊢ ∀ (n : ℕ), (f : (a : R) → S) (a ^ n) = HPow.hPow (α := S) ((f : (a : R) → S) a : S) n

Tactic:
map_pow f a

Premises used: map_pow
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Add R
inst_1 : Add S
inst_2 : Mul R
inst_3 : Mul S
e : R ≃+* S
⊢ e.trans e.symm = refl R

Tactic:
ext e.left_inv

Premises used: RingEquiv.toEquiv, RingEquiv.ext, Equiv.left_inv
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Add R
inst_1 : Add S
inst_2 : Mul R
inst_3 : Mul S
e : R ≃+* S
⊢ e.symm.trans e = refl S

Tactic:
ext e.right_inv

Premises used: RingEquiv.toEquiv, Equiv.right_inv, RingEquiv.ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
g : S →ₙ+* R
h₁ : g.comp f = NonUnitalRingHom.id R
h₂ : f.comp g = NonUnitalRingHom.id S
⊢ (ofNonUnitalRingHom f g h₁ h₂).symm = ofNonUnitalRingHom g f h₂ h₁

Tactic:
rfl

Premises used: RingEquiv.ofNonUnitalRingHom, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
g : S →+* R
h₁ : f.comp g = RingHom.id S
h₂ : g.comp f = RingHom.id R
⊢ (↑(ofRingHom f g h₁ h₂) : R →+* S) = f

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
g : S →+* R
h₁ : RingHom.comp (↑f : R →+* S) g = RingHom.id S
h₂ : g.comp (↑f : R →+* S) = RingHom.id R
⊢ ofRingHom (↑f : R →+* S) g h₁ h₂ = f

Tactic:
ext fun _ ↦ rfl

Premises used: RingEquiv.ext, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
g : S →+* R
h₁ : f.comp g = RingHom.id S
h₂ : g.comp f = RingHom.id R
⊢ (ofRingHom f g h₁ h₂).symm = ofRingHom g f h₂ h₁

Tactic:
rfl

Premises used: RingEquiv.ofRingHom, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
α : Type u_2
β : Type u_3
R : Type u_4
inst : NonAssocSemiring R
x : α ⊕ β → R
⊢ Eq (α := (α → R) × (β → R))
    ((sumArrowEquivProdArrow α β R : (a : α ⊕ β → R) → (α → R) × (β → R)) x : (α → R) × (β → R))
    ((Equiv.sumArrowEquivProdArrow α β R : (a : α ⊕ β → R) → (α → R) × (β → R)) x : (α → R) × (β → R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
α : Type u_2
β : Type u_3
R : Type u_4
inst : NonAssocSemiring R
x : (α → R) × (β → R)
⊢ Eq (α := α ⊕ β → R)
    ((RingEquiv.symm (sumArrowEquivProdArrow α β R) : (a : (α → R) × (β → R)) → α ⊕ β → R) x : α ⊕ β → R)
    (((Equiv.sumArrowEquivProdArrow α β R).symm : (a : (α → R) × (β → R)) → α ⊕ β → R) x : α ⊕ β → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
A : Type u_7
B : Type u_8
inst : MulZeroClass A
inst_1 : MulZeroClass B
inst_2 : NoZeroDivisors B
e : A ≃* B
⊢ NoZeroDivisors A

Tactic:
e.injective.noZeroDivisors e (map_zero e) (map_mul e)

Premises used: map_zero, map_mul, Function.Injective.noZeroDivisors, DFunLike.coe, MulEquiv.injective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
A : Type u_7
B : Type u_8
inst : Semiring A
inst_1 : Semiring B
inst_2 : IsDomain B
e : A ≃* B
⊢ IsDomain A

Tactic:
{ e.injective.isLeftCancelMulZero e (map_zero e) (map_mul e),
    e.injective.isRightCancelMulZero e (map_zero e) (map_mul e) with
    exists_pair_ne := ⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩ }

Premises used: map_zero, IsDomain.mk, map_mul, Function.Injective.isLeftCancelMulZero, Function.Injective.isRightCancelMulZero, DFunLike.coe, MulEquiv.injective
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Distrib R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
rcases :
  ∀ (mul add : 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) (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
    (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
    { mul := mul, add := add, left_distrib := left_distrib, right_distrib := right_distrib : Distrib R } = inst₂
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨⟨⟩, ⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : Distrib R
mul add : 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
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
rcases :
  ∀ (mul_1 add_1 : R → R → R) (left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c)
    (right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c) (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
    (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
    { mul := mul, add := add, left_distrib := left_distrib, right_distrib := right_distrib : Distrib R } =
      { mul := mul_1, add := add_1, left_distrib := left_distrib_1, right_distrib := right_distrib_1 }
⊢ { mul := mul, add := add, left_distrib := left_distrib, right_distrib := right_distrib : Distrib R } = inst₂

Tactic:
rcases inst₂ with @⟨⟨⟩, ⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
mul add : 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
mul_1 add_1 : R → R → R
left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ { mul := mul, add := add, left_distrib := left_distrib, right_distrib := right_distrib : Distrib R } =
    { mul := mul_1, add := add_1, left_distrib := left_distrib_1, right_distrib := right_distrib_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonUnitalNonAssocSemiring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
rcases :
  ∀ [toAddCommMonoid : AddCommMonoid 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 : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
    (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
    { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
        zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring R } =
      inst₂
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨_, ⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : NonUnitalNonAssocSemiring R
toAddCommMonoid : AddCommMonoid 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 : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
rcases :
  ∀ [toAddCommMonoid_1 : AddCommMonoid R] (mul_1 : R → R → R)
    (left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c)
    (right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c) (zero_mul_1 : ∀ (a : R), 0 * a = 0)
    (mul_zero_1 : ∀ (a : R), a * 0 = 0) (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
    (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
    { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
        zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring R } =
      { toAddCommMonoid := toAddCommMonoid_1, mul := mul_1, left_distrib := left_distrib_1,
        right_distrib := right_distrib_1, zero_mul := zero_mul_1, mul_zero := mul_zero_1 }
⊢ { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring R } =
    inst₂

Tactic:
rcases inst₂ with @⟨_, ⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommMonoid : AddCommMonoid 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
toAddCommMonoid_1 : AddCommMonoid R
mul_1 : R → R → R
left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
e_toAddCommMonoid : toAddCommMonoid = toAddCommMonoid_1
⊢ { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring R } =
    { toAddCommMonoid := toAddCommMonoid_1, mul := mul_1, left_distrib := left_distrib_1,
      right_distrib := right_distrib_1, zero_mul := zero_mul_1, mul_zero := mul_zero_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommMonoid : AddCommMonoid 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
toAddCommMonoid_1 : AddCommMonoid R
mul_1 : R → R → R
left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
e_toAddCommMonoid : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
⊢ toAddCommMonoid = toAddCommMonoid_1

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommMonoid : AddCommMonoid 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
toAddCommMonoid_1 : AddCommMonoid R
mul_1 : R → R → R
left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ : NonUnitalNonAssocSemiring R
_ : ∀ ⦃a₂ : NonUnitalNonAssocSemiring R⦄, Eq.{u + 1} (α := Distrib R) toDistrib toDistrib → a₁ = a₂
⊢ ∀ ⦃a₂ : NonUnitalNonAssocSemiring R⦄, Eq.{u + 1} (α := Distrib R) toDistrib toDistrib → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocSemiring R
h : Eq.{u + 1} (α := Distrib R) toDistrib toDistrib
h_add : ∀ (x y : R), x + y = x + y
h_mul : ∀ (x y : R), x * y = x * y
⊢ a₁ = a₂

Tactic:
ext x y
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocSemiring R
h : Eq.{u + 1} (α := Distrib R) toDistrib toDistrib
x y : R
⊢ x + y = x + y

Tactic:
congrArg (·.toAdd.add x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocSemiring R
h : Eq.{u + 1} (α := Distrib R) toDistrib toDistrib
x y : R
⊢ x + y = x + y

Tactic:
exact congrArg (·.toAdd.add x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocSemiring R
h : Eq.{u + 1} (α := Distrib R) toDistrib toDistrib
x y : R
⊢ x * y = x * y

Tactic:
congrArg (·.toMul.mul x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocSemiring R
h : Eq.{u + 1} (α := Distrib R) toDistrib toDistrib
x y : R
⊢ x * y = x * y

Tactic:
exact congrArg (·.toMul.mul x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring R
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocSemiring_1 : NonUnitalNonAssocSemiring R
mul_assoc_1 : ∀ (a b c : R), a * b * c = a * (b * c)
h :
  Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) NonUnitalSemiring.toNonUnitalNonAssocSemiring
    NonUnitalSemiring.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring, mul_assoc := mul_assoc : NonUnitalSemiring R } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring_1, mul_assoc := mul_assoc_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonUnitalSemiring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ inst₁ = inst₂

Tactic:
toNonUnitalNonAssocSemiring_injective <|
    NonUnitalNonAssocSemiring.ext h_add h_mul

Premises used: NonUnitalSemiring.toNonUnitalNonAssocSemiring_injective, NonUnitalNonAssocSemiring.ext
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
⊢ Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
exact h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid

Tactic:
have h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid := by ext : 1; exact h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
⊢ Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero

Tactic:
have h_zero' : inst₁.toZero = inst₂.toZero := congrArg (·.toZero) h_monoid
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
⊢ Eq.{u + 1} (α := One R) toOne toOne

Tactic:
have h_one' : inst₁.toOne = inst₂.toOne :=
    congrArg One.mk h_one
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) ↑n ↑n
⊢ Eq.{u + 1} (α := ℕ → R) NatCast.natCast NatCast.natCast

Tactic:
funext n
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
h : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) ↑0 ↑0

Tactic:
rewrite [inst₁.natCast_zero, inst₂.natCast_zero]

Premises used: AddMonoidWithOne.natCast_zero
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
⊢ Eq.{u + 1} (α := R) 0 0

Tactic:
congrArg (@Zero.zero R) h_zero'

Premises used: congrArg, Zero.zero