awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
⊢ toSub = toSub_1

Tactic:
injection h₃
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
⊢ zsmul = zsmul_1

Tactic:
injection h₃
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
⊢ toIntCast = toIntCast_1

Tactic:
injection h₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
⊢ toIntCast = toIntCast_1

Tactic:
solve | injection h₂ | injection h₃
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ : Ring R
_ : ∀ ⦃a₂ : Ring R⦄, Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing → a₁ = a₂
⊢ ∀ ⦃a₂ : Ring R⦄, Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing
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
a₁ : Ring R
_ : ∀ ⦃a₂ : Ring R⦄, Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing → a₁ = a₂
⊢ ∀ ⦃a₂ : Ring R⦄, Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
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₂ : Ring R
h : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
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
a₁ : Ring R
_ : ∀ ⦃a₂ : Ring R⦄, Eq.{u + 1} (α := Semiring R) toSemiring toSemiring → a₁ = a₂
⊢ ∀ ⦃a₂ : Ring R⦄, Eq.{u + 1} (α := Semiring R) toSemiring toSemiring → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
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₂ : Ring R
h : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
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₂ : Ring R
h : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
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₂ : Ring R
h : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
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₂ : Ring R
h : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
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_comm : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocSemiring_1 : NonUnitalNonAssocSemiring R
mul_comm_1 : ∀ (a b : R), a * b = b * a
h :
  Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring
    NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring, mul_comm := mul_comm :
      NonUnitalNonAssocCommSemiring R } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring_1, mul_comm := mul_comm_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonUnitalNonAssocCommSemiring 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: NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring_injective, NonUnitalNonAssocSemiring.ext
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalSemiring : NonUnitalSemiring R
mul_comm : ∀ (a b : R), a * b = b * a
toNonUnitalSemiring_1 : NonUnitalSemiring R
mul_comm_1 : ∀ (a b : R), a * b = b * a
h :
  Eq.{u + 1} (α := NonUnitalSemiring R) NonUnitalCommSemiring.toNonUnitalSemiring
    NonUnitalCommSemiring.toNonUnitalSemiring
⊢ { toNonUnitalSemiring := toNonUnitalSemiring, mul_comm := mul_comm : NonUnitalCommSemiring R } =
    { toNonUnitalSemiring := toNonUnitalSemiring_1, mul_comm := mul_comm_1 }

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

Tactic:
toNonUnitalSemiring_injective <|
    NonUnitalSemiring.ext h_add h_mul

Premises used: NonUnitalSemiring.ext, NonUnitalCommSemiring.toNonUnitalSemiring_injective
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing R
mul_comm : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing R
mul_comm_1 : ∀ (a b : R), a * b = b * a
h :
  Eq.{u + 1} (α := NonUnitalNonAssocRing R) NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
    NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, mul_comm := mul_comm : NonUnitalNonAssocCommRing R } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing_1, mul_comm := mul_comm_1 }

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

Tactic:
toNonUnitalNonAssocRing_injective <|
    NonUnitalNonAssocRing.ext h_add h_mul

Premises used: NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing_injective, NonUnitalNonAssocRing.ext
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalRing : NonUnitalRing R
mul_comm : ∀ (a b : R), a * b = b * a
toNonUnitalRing_1 : NonUnitalRing R
mul_comm_1 : ∀ (a b : R), a * b = b * a
h : Eq.{u + 1} (α := NonUnitalRing R) NonUnitalCommRing.toNonUnitalRing NonUnitalCommRing.toNonUnitalRing
⊢ { toNonUnitalRing := toNonUnitalRing, mul_comm := mul_comm : NonUnitalCommRing R } =
    { toNonUnitalRing := toNonUnitalRing_1, mul_comm := mul_comm_1 }

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

Tactic:
toNonUnitalRing_injective <|
    NonUnitalRing.ext h_add h_mul

Premises used: NonUnitalRing.ext, NonUnitalCommRing.toNonUnitalRing_injective
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toSemiring : Semiring R
mul_comm : ∀ (a b : R), a * b = b * a
toSemiring_1 : Semiring R
mul_comm_1 : ∀ (a b : R), a * b = b * a
h : Eq.{u + 1} (α := Semiring R) CommSemiring.toSemiring CommSemiring.toSemiring
⊢ { toSemiring := toSemiring, mul_comm := mul_comm : CommSemiring R } =
    { toSemiring := toSemiring_1, mul_comm := mul_comm_1 }

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

Tactic:
toSemiring_injective <|
    Semiring.ext h_add h_mul

Premises used: Semiring.ext, CommSemiring.toSemiring_injective
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toRing : Ring R
mul_comm : ∀ (a b : R), a * b = b * a
toRing_1 : Ring R
mul_comm_1 : ∀ (a b : R), a * b = b * a
h : Eq.{u + 1} (α := Ring R) CommRing.toRing CommRing.toRing
⊢ { toRing := toRing, mul_comm := mul_comm : CommRing R } = { toRing := toRing_1, mul_comm := mul_comm_1 }

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

Tactic:
toRing_injective <| Ring.ext h_add h_mul

Premises used: CommRing.toRing_injective, Ring.ext
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
⊢ ∑ i ∈ range (n + 1), x ^ i = x * ∑ i ∈ range n, x ^ i + 1

Tactic:
simp only [mul_sum, ← pow_succ', sum_range_succ', pow_zero]

Premises used: Finset.mul_sum, pow_zero, Finset.sum_range_succ', pow_succ'
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
⊢ ∑ i ∈ range (n + 1), x ^ i = x ^ n + ∑ i ∈ range n, x ^ i

Tactic:
(sum_range_succ _ _).trans (add_comm _ _)

Premises used: add_comm, Finset.sum_range_succ, Eq.trans
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i) 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, List.foldr, Finset.sum, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range 1, x ^ i) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
⊢ ∑ i ∈ range 2, x ^ i = x + 1

Tactic:
simp [geom_sum_succ']

Premises used: geom_sum_succ'
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, HPow.hPow (α := R) 0 i) (if Eq (α := ℕ) 0 0 then 0 else 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range 1, HPow.hPow (α := R) 0 i) (if Eq (α := ℕ) 1 0 then 0 else 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
rw : HPow.hPow (α := R) 0 (n + 1) + ∑ i ∈ range (n + 1), HPow.hPow (α := R) 0 i = if n + 2 = 0 then 0 else 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range (n + 2), HPow.hPow (α := R) 0 i) (if n + 2 = 0 then 0 else 1)

Tactic:
rw [geom_sum_succ']

Premises used: geom_sum_succ'
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ HPow.hPow (α := R) 0 (n + 1) + ∑ i ∈ range (n + 1), HPow.hPow (α := R) 0 i = if n + 2 = 0 then 0 else 1

Tactic:
simp [zero_geom_sum]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, HPow.hPow (α := R) 1 i) (↑n : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (∑ i ∈ range n, x ^ i)) (∑ i ∈ range n, op x ^ i)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
rw :
  Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j))
    (∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i))
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i) (∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i))

Tactic:
rw [← sum_range_reflect]

Premises used: Finset.sum_range_reflect
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j))
    (∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i))

Tactic:
sum_congr rfl fun j j_in => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
refine :
  ∀ (j : ℕ) (j_in : j ∈ range n), op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j))
    (∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i))

Tactic:
refine sum_congr rfl fun j j_in => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
n j : ℕ
j_in : j ∈ range n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n i : ℕ
h : i ∈ range n
rw : x ^ i * 1 = x ^ i
rw₁ rw₂ : x ^ i = x ^ i
⊢ x ^ i * HPow.hPow (α := R) 1 (n - 1 - i) = x ^ i

Tactic:
rw [one_pow, mul_one]

Premises used: one_pow, mul_one
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
change : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
change (∑ i ∈ range n, (f n) i) * x + y ^ n = (x + y) ^ n

Premises used: Finset.range, HAdd.hAdd, Finset.sum
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
zero : (∑ i ∈ ∅, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₁ : 0 * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₂ : 0 + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₃ : HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₄ : 1 = HPow.hPow (β := ℕ) (x + y) 0
zero₅ zero₆ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0

Tactic:
rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]

Premises used: MulZeroClass.zero_mul, zero_add, pow_zero, Finset.sum_empty, Finset.range_zero
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
dsimp : (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n
⊢ f (n + 1) n = (x + y) ^ n

Tactic:
dsimp only [f]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
rw : (x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n
rw₁ : (x + y) ^ n * y ^ (1 + n - (1 + n)) = (x + y) ^ n
rw₂ : (x + y) ^ n * HPow.hPow (β := ℕ) y 0 = (x + y) ^ n
rw₃ : (x + y) ^ n * 1 = (x + y) ^ n
rw₄ rw₅ : (x + y) ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n

Tactic:
rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]

Premises used: tsub_self, pow_zero, tsub_add_eq_tsub_tsub, mul_one, Nat.add_comm
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ f (n + 1) n = (x + y) ^ n

Tactic:
have f_last : f (n + 1) n = (x + y) ^ n := by
      dsimp only [f]
      rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
dsimp : (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))
⊢ f (n + 1) i = y * f n i

Tactic:
dsimp only [f]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ Commute y ((x + y) ^ i)

Tactic:
have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
rw : (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))

Tactic:
rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]

Premises used: mul_assoc, HSub.hSub, add_comm, tsub_add_eq_tsub_tsub, add_tsub_cancel_right, OfNat.ofNat, Commute.eq, pow_succ'
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ i + 1 + (n - (i + 1)) = n

Tactic:
have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)