awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n

Tactic:
Dvd.intro_left _ h₁

Premises used: Dvd.intro_left
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n

Tactic:
exact Dvd.intro_left _ h₁

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

Tactic:
(Commute.all x y).geom_sum₂_succ_eq

Premises used: Commute.geom_sum₂_succ_eq, Commute.all
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommRing R
x y : R
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)

Tactic:
(Commute.all x y).mul_geom_sum₂_Ico hmn

Premises used: Commute.mul_geom_sum₂_Ico, Commute.all
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
inl : ∀ (h : y ≤ x), x - y ∣ x ^ n - y ^ n
inr : ∀ (h : x < y), x - y ∣ x ^ n - y ^ n
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
rcases le_or_gt y x with h | h

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
h : y ≤ x
⊢ y ^ n ≤ x ^ n

Tactic:
have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n

Premises used: Dvd.dvd, congrArg, Nat.cast_sub._simp_1, HSub.hSub, cast, Nat.cast, congr, sub_dvd_pow_sub_pow, Eq.trans, Int.ofNat_dvd._simp_1, Nat.cast_pow._simp_1
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n

Premises used: Nat.cast, sub_dvd_pow_sub_pow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
h : x < y
⊢ x ^ n ≤ y ^ n

Tactic:
have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
(Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)

Premises used: dvd_zero, HSub.hSub, Eq.rec, Eq.symm, Nat.sub_eq_zero_of_le
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x n : ℕ
⊢ x - 1 ∣ x ^ n - 1

Tactic:
simpa using x.sub_dvd_pow_sub_pow 1 n

Premises used: Nat.sub_dvd_pow_sub_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
m k x y : ℕ
hmk : m ∣ k
obtain : ∀ (n : ℕ), x ^ m - y ^ m ∣ x ^ (m * n) - y ^ (m * n)
⊢ x ^ m - y ^ m ∣ x ^ k - y ^ k

Tactic:
obtain ⟨n, rfl⟩ := hmk

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
m x y n : ℕ
⊢ x ^ m - y ^ m ∣ x ^ (m * n) - y ^ (m * n)

Tactic:
simpa [pow_mul] using (x ^ m).sub_dvd_pow_sub_pow (y ^ m) n

Premises used: Nat.sub_dvd_pow_sub_pow, pow_mul, HPow.hPow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
m k x : ℕ
hmk : m ∣ k
⊢ x ^ m - 1 ∣ x ^ k - 1

Tactic:
simpa using pow_sub_pow_dvd_pow_sub_pow x 1 hmk

Premises used: Nat.pow_sub_pow_dvd_pow_sub_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
x y n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n

Tactic:
mod_cast Odd.add_dvd_pow_add_pow (x : ℤ) (↑y) h

Premises used: Dvd.dvd, congrArg, Nat.cast_add._simp_1, cast, Nat.cast, HPow.hPow, HAdd.hAdd, congr, Odd.add_dvd_pow_add_pow, Eq.trans, Int.ofNat_dvd._simp_1, Nat.cast_pow._simp_1
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)

Tactic:
(Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm

Premises used: Iff.mpr, tsub_pos_iff_lt, tsub_eq_of_eq_add, Nat.div_eq_of_eq_mul_left, Eq.symm
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
m : ℕ
hm : 2 ≤ m
n : ℕ
refine : m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1
⊢ ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)

Tactic:
refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm

Premises used: Iff.mpr, tsub_pos_iff_lt, tsub_eq_of_eq_add, Nat.div_eq_of_eq_mul_left, Eq.symm
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ 1 ≤ m

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1

Tactic:
simpa only [tsub_add_cancel_of_le (by lia : 1 ≤ m), eq_comm] using geom_sum_mul_add (m - 1) n

Premises used: HSub.hSub, tsub_add_cancel_of_le, eq_comm, geom_sum_mul_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
⊢ ∀ (a : α), a + 0 = a

Tactic:
simp [add_zero]

Premises used: add_zero
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
⊢ ∀ (a : α), a * 1 = a

Tactic:
simp [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
⊢ ∀ (a : α), 0 * a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
a : α
⊢ HPow.hPow (β := ℕ) a 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
a : α
n : ℕ
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
⊢ OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1) = HAdd.hAdd (α := α) (OfNat.ofNat 0) 1

Tactic:
simp [zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
change : (↑2 : α) = HAdd.hAdd (α := α) 1 1
⊢ OfNat.ofNat (HAdd.hAdd (α := ℕ) 1 1) = HAdd.hAdd (α := α) (OfNat.ofNat 1) 1

Tactic:
change Nat.cast 2 = 1 + 1

Premises used: Nat.cast, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
rw : Eq.{u_1 + 1} (α := α) (↑2 : α) 2
⊢ (↑2 : α) = HAdd.hAdd (α := α) 1 1

Tactic:
rw [one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
⊢ Eq.{u_1 + 1} (α := α) (↑2 : α) 2

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
n : ℕ
change : (↑(n + 2 + 1) : α) = HAdd.hAdd (α := α) (↑(n + 2) : α) 1
⊢ OfNat.ofNat (n + 2 + 1) = HAdd.hAdd (α := α) (OfNat.ofNat (n + 2)) 1

Tactic:
change Nat.cast (n + 2 + 1) = Nat.cast (n + 2) + 1

Premises used: Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Semiring α
n : ℕ
rw rw₁ : Eq.{u_1 + 1} (α := α) (↑(n + 2 + 1) : α) ↑(n + 2 + 1)
⊢ (↑(n + 2 + 1) : α) = HAdd.hAdd (α := α) (↑(n + 2) : α) 1

Tactic:
rw [← AddMonoidWithOne.natCast_succ]

Premises used: AddMonoidWithOne.natCast_succ
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Ring α
⊢ ∀ (a : α), -a + a = 0

Tactic:
simp [neg_add_cancel]

Premises used: neg_add_cancel
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (OfNat.ofNat 0) (↑0 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (OfNat.ofNat 1) (↑1 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
inst : Semiring α
n_1 n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (OfNat.ofNat (n + 2)) (↑(n + 2) : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (OfNat.ofNat n) (↑n : α)

Tactic:
match n with
  | 0 => simp
  | 1 => simp
  | n + 2 => rfl
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
s : Grind.CommRing α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α) (-(↑(n + 1) : α))
rw₁ : Eq.{u_1 + 1} (α := α) (-(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α)) (-(↑(n + 1) : α))
rw₂ : -HAdd.hAdd (α := α) (↑n : α) 1 = -(↑(n + 1) : α)
rw₃ rw₄ : -HAdd.hAdd (α := α) (↑n : α) 1 = -HAdd.hAdd (α := α) (↑n : α) 1
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.negSucc n) : α) (-(↑(n + 1) : α))

Tactic:
rw [Int.negSucc_eq, Grind.Ring.intCast_neg,
        Grind.Ring.intCast_natCast_add_one, Grind.Semiring.natCast_succ]

Premises used: Lean.Grind.Ring.intCast_natCast_add_one, Lean.Grind.Ring.intCast_neg, Lean.Grind.Semiring.natCast_succ, Int.negSucc_eq
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
⊢ Eq (α := Grind.Semiring ℕ) inferInstance Grind.CommSemiring.toSemiring

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.GrindInstances
Goal:
α : Type u_1
⊢ Eq (α := Grind.Semiring UInt8) inferInstance Grind.CommSemiring.toSemiring

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f g : α →ₙ+* β
h : Eq (α := (a : α) → β) ((fun (f : α →ₙ+* β) ↦ f.toFun) f) ((fun (f : α →ₙ+* β) ↦ f.toFun) g)
mk :
  ∀ (toMulHom : α →ₙ* β) (map_zero' : toMulHom.toFun 0 = 0)
    (map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
        ((fun (f : α →ₙ+* β) ↦ f.toFun) g)),
    { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
g : α →ₙ+* β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) g)
mk :
  ∀ (toMulHom_1 : α →ₙ* β) (map_zero'_1 : toMulHom_1.toFun 0 = 0)
    (map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
        ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })),
    { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } =
      { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }
⊢ { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
toMulHom_1 : α →ₙ* β
map_zero'_1 : toMulHom_1.toFun 0 = 0
map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
mk : toMulHom = toMulHom_1
⊢ { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } =
    { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
toMulHom_1 : α →ₙ* β
map_zero'_1 : toMulHom_1.toFun 0 = 0
map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
mk : Eq (α := (a : α) → β) (⇑toMulHom : (a : α) → β) (⇑toMulHom_1 : (a : α) → β)
⊢ toMulHom = toMulHom_1

Tactic:
apply DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
toMulHom_1 : α →ₙ* β
map_zero'_1 : toMulHom_1.toFun 0 = 0
map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ Eq (α := (a : α) → β) (⇑toMulHom : (a : α) → β) (⇑toMulHom_1 : (a : α) → β)

Tactic:
h
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
toMulHom_1 : α →ₙ* β
map_zero'_1 : toMulHom_1.toFun 0 = 0
map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ Eq (α := (a : α) → β) (⇑toMulHom : (a : α) → β) (⇑toMulHom_1 : (a : α) → β)

Tactic:
exact h
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α →ₙ+* β
⊢ Eq (α := (a : α) → β) (⇑f.toMulHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α → β
h₁ : ∀ (x y : α), f (x * y) = f x * f y
h₂ : { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun 0 = 0
h₃ :
  ∀ (x y : α),
    { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun (x + y) =
      { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun x + { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun y
⊢ (↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : α →ₙ+* β } : α →ₙ* β) =
    { toFun := f, map_mul' := h₁ : α →ₙ* β }

Tactic:
rfl

Premises used: MulHomClass.toMulHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α →ₙ+* β
⊢ Eq (α := (a : α) → β) (⇑f.toAddMonoidHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α → β
h₁ : ∀ (x y : α), f (x * y) = f x * f y
h₂ : { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun 0 = 0
h₃ :
  ∀ (x y : α),
    { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun (x + y) =
      { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun x + { toFun := f, map_mul' := h₁ : α →ₙ* β }.toFun y
⊢ (↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : α →ₙ+* β } : α →+ β) =
    { toFun := f, map_zero' := h₂, map_add' := h₃ : α →+ β }

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α →ₙ+* β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α →ₙ+* β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f g : α →ₙ+* β
⊢ (∀ (x : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) → f = g

Tactic:
DFunLike.ext _ _

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α →ₙ+* β
h₁ :
  ∀ (x y : α),
    (f : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
h₂ : { toFun := (⇑f : (a : α) → β), map_mul' := h₁ : α →ₙ* β }.toFun 0 = 0
h₃ :
  ∀ (x y : α),
    { toFun := (⇑f : (a : α) → β), map_mul' := h₁ : α →ₙ* β }.toFun (x + y) =
      { toFun := (⇑f : (a : α) → β), map_mul' := h₁ : α →ₙ* β }.toFun x +
        { toFun := (⇑f : (a : α) → β), map_mul' := h₁ : α →ₙ* β }.toFun y
⊢ { toFun := (⇑f : (a : α) → β), map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : α →ₙ+* β } = f

Tactic:
ext fun _ => rfl

Premises used: NonUnitalRingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
⊢ Injective (β := α →+ β) fun (f : α →ₙ+* β) ↦ (↑f : α →+ β)

Tactic:
Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
⊢ Injective (β := α →ₙ* β) fun (f : α →ₙ+* β) ↦ (↑f : α →ₙ* β)

Tactic:
Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
⊢ Eq (α := (a : α) → β) (⇑0 : (a : α) → β) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((0 : (a : α) → β) x : β) (0 : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
inst : NonUnitalNonAssocSemiring α
x : α
⊢ (NonUnitalRingHom.id α : (a : α) → α) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
inst : NonUnitalNonAssocSemiring α
⊢ Eq (α := α →+ α) (↑(NonUnitalRingHom.id α) : α →+ α) (AddMonoidHom.id α)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
inst : NonUnitalNonAssocSemiring α
⊢ Eq (α := α →ₙ* α) (↑(NonUnitalRingHom.id α) : α →ₙ* α) (MulHom.id α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
δ : Type u_5
x : NonUnitalNonAssocSemiring δ
f : α →ₙ+* β
g : β →ₙ+* γ
h : γ →ₙ+* δ
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f : α →ₙ+* β
⊢ Eq (α := (a : α) → γ) (⇑(g.comp f) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f : α →ₙ+* β
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((g.comp f : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f : (a : α) → β) x : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f : α →ₙ+* β
⊢ { toFun := Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β), map_zero' := ⋯,
      map_add' := ⋯ : α →+ γ } =
    AddMonoidHom.comp (↑g : β →+ γ) (↑f : α →+ β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f : α →ₙ+* β
⊢ { toFun := Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β), map_mul' := ⋯ :
      α →ₙ* γ } =
    MulHom.comp (↑g : β →ₙ* γ) (↑f : α →ₙ* β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
a : ∀ (x : α), Eq.{u_4 + 1} (α := γ) ((g.comp 0 : (a : α) → γ) x : γ) ((0 : (a : α) → γ) x : γ)
⊢ Eq (α := α →ₙ+* γ) (g.comp 0) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((g.comp 0 : (a : α) → γ) x : γ) ((0 : (a : α) → γ) x : γ)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
a : ∀ (x : α), Eq.{u_4 + 1} (α := γ) ((comp 0 f : (a : α) → γ) x : γ) ((0 : (a : α) → γ) x : γ)
⊢ Eq (α := α →ₙ+* γ) (comp 0 f) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((comp 0 f : (a : α) → γ) x : γ) ((0 : (a : α) → γ) x : γ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α →ₙ+* β
⊢ f.comp (NonUnitalRingHom.id α) = f

Tactic:
ext fun _ => rfl

Premises used: NonUnitalRingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f : α →ₙ+* β
⊢ comp (NonUnitalRingHom.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: NonUnitalRingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
inst : NonUnitalNonAssocSemiring α
⊢ Eq (α := α →ₙ+* α) 1 (NonUnitalRingHom.id α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
inst : NonUnitalNonAssocSemiring α
⊢ Eq.{u_2 + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
inst : NonUnitalNonAssocSemiring α
f g : α →ₙ+* α
⊢ f * g = f.comp g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
inst : NonUnitalNonAssocSemiring α
f g : α →ₙ+* α
⊢ Eq (α := (a : α) → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))

Tactic:
rfl

Premises used: rfl