awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ g₂ : β →ₙ+* γ
f : α →ₙ+* β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 (NonUnitalRingHom.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, Eq.rec, NonUnitalRingHom.ext, NonUnitalRingHom.ext_iff, Iff.intro, Iff.mp, 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₁ f₂ : α →ₙ+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: NonUnitalRingHom.comp_apply
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : FunLike F α β
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
inst_1 : RingHomClass F α β
⊢ NonUnitalRingHomClass F α β

Tactic:
{ ‹RingHomClass F α β› with }

Premises used: NonUnitalRingHomClass.mk
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f g : α →+* β
h :
  Eq (α := (a : α) → β) ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) f)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)
mk :
  ∀ (toMonoidHom : α →* β) (map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0)
    (map_add' :
      ∀ (x_2 y : α),
        (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
          (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
          { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
        ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)),
    { toMonoidHom := toMonoidHom, 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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
g : α →+* β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)
mk :
  ∀ (toMonoidHom_1 : α →* β) (map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0)
    (map_add'_1 :
      ∀ (x_2 y : α),
        (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
          (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
          { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
        ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
          { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })),
    { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' : α →+* β } =
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }
⊢ { toMonoidHom := toMonoidHom, 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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
toMonoidHom_1 : α →* β
map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0
map_add'_1 :
  ∀ (x_2 y : α),
    (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
mk : toMonoidHom = toMonoidHom_1
⊢ { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' : α →+* β } =
    { toMonoidHom := toMonoidHom_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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
toMonoidHom_1 : α →* β
map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0
map_add'_1 :
  ∀ (x_2 y : α),
    (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
mk : Eq (α := (a : α) → β) (⇑toMonoidHom : (a : α) → β) (⇑toMonoidHom_1 : (a : α) → β)
⊢ toMonoidHom = toMonoidHom_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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
toMonoidHom_1 : α →* β
map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0
map_add'_1 :
  ∀ (x_2 y : α),
    (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ Eq (α := (a : α) → β) (⇑toMonoidHom : (a : α) → β) (⇑toMonoidHom_1 : (a : α) → β)

Tactic:
h
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
toMonoidHom_1 : α →* β
map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0
map_add'_1 :
  ∀ (x_2 y : α),
    (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ Eq (α := (a : α) → β) (⇑toMonoidHom : (a : α) → β) (⇑toMonoidHom_1 : (a : α) → β)

Tactic:
exact h
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ (↑f.toMonoidHom : OneHom α β).toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →* β
h₁ : (↑f : OneHom α β).toFun 0 = 0
h₂ : ∀ (x_2 y : α), (↑f : OneHom α β).toFun (x_2 + y) = (↑f : OneHom α β).toFun x_2 + (↑f : OneHom α β).toFun y
⊢ Eq (α := (a : α) → β) (⇑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ : α →+* β } : (a : α) → β)
    (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
F : Type u_5
inst : FunLike F α β
inst_1 : RingHomClass F α β
f : F
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →+* β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ (↑f : α →* β) = (↑f : α →* β)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ Eq (α := (a : α) → β) (⇑f.toMonoidWithZeroHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →* β
h₁ : (↑f : OneHom α β).toFun 0 = 0
h₂ : ∀ (x_2 y : α), (↑f : OneHom α β).toFun (x_2 + y) = (↑f : OneHom α β).toFun x_2 + (↑f : OneHom α β).toFun y
⊢ (↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ : α →+* β } : α →* β) = f

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ f.toAddMonoidHom = (↑f : α →+ β)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α → β
h₁ : f 1 = 1
h₂ :
  ∀ (x_2 y : α),
    { toFun := f, map_one' := h₁ : OneHom α β }.toFun (x_2 * y) =
      { toFun := f, map_one' := h₁ : OneHom α β }.toFun x_2 * { toFun := f, map_one' := h₁ : OneHom α β }.toFun y
h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun 0 = 0
h₄ :
  ∀ (x_2 y : α),
    (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun (x_2 + y) =
      (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun x_2 +
        (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun y
⊢ (↑{ toFun := f, map_one' := h₁, 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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
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
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
f g : α →+* β
h : f = g
x : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
f : α →+* β
x y : α
h : x = y
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
DFunLike.congr_arg f h

Premises used: DFunLike.congr_arg
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f g : α →+* β
h : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
⊢ f = g

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f g : α →+* β
⊢ (∀ (x_2 : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x_2 : β) ((g : (a : α) → β) x_2 : β)) → f = g

Tactic:
DFunLike.ext _ _

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
h₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
h₂ :
  ∀ (x_2 y : α),
    { toFun := (⇑f : (a : α) → β), map_one' := h₁ : OneHom α β }.toFun (x_2 * y) =
      { toFun := (⇑f : (a : α) → β), map_one' := h₁ : OneHom α β }.toFun x_2 *
        { toFun := (⇑f : (a : α) → β), map_one' := h₁ : OneHom α β }.toFun y
h₃ : (↑{ toFun := (⇑f : (a : α) → β), map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun 0 = 0
h₄ :
  ∀ (x_2 y : α),
    (↑{ toFun := (⇑f : (a : α) → β), map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun (x_2 + y) =
      (↑{ toFun := (⇑f : (a : α) → β), map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun x_2 +
        (↑{ toFun := (⇑f : (a : α) → β), map_one' := h₁, map_mul' := h₂ : α →* β } : OneHom α β).toFun y
⊢ { toFun := (⇑f : (a : α) → β), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ : α →+* β } = f

Tactic:
ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
⊢ Injective (β := α →+ β) fun (f : α →+* β) ↦ (↑f : α →+ β)

Tactic:
fun _ _ h =>
  ext <| DFunLike.congr_fun (F := α →+ β) h

Premises used: DFunLike.congr_fun, RingHom.ext, Function.Injective
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
⊢ 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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)

Tactic:
map_one f

Premises used: map_one
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ ∀ (a b : α),
    (f : (a : α) → β) (a + b) = HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
map_add f

Premises used: map_add
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ ∀ (a b : α),
    (f : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
map_mul f

Premises used: map_mul
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
rw : Eq.{u_3 + 1} (α := β) 0 1 ↔ Eq.{u_3 + 1} (α := β) 1 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := β) 1 0 ↔ Eq.{u_3 + 1} (α := β) 1 0
⊢ Eq.{u_3 + 1} (α := β) 0 1 ↔ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)

Tactic:
rw [map_one, eq_comm]

Premises used: eq_comm, map_one
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
f : α →+* β
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
x : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x * 1) : β) (0 : β)
rw₁ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) 1 : β) = 0
rw₂ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) (0 : β) = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := β) 0 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) (0 : β)

Tactic:
rw [← mul_one x, map_mul, h, mul_zero]

Premises used: MulZeroClass.mul_zero, map_mul, mul_one
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
inst : Nontrivial β
⊢ Ne.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)

Tactic:
mt f.codomain_trivial_iff_map_one_eq_zero.mpr zero_ne_one

Premises used: Iff.mpr, mt, zero_ne_one, RingHom.codomain_trivial_iff_map_one_eq_zero
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
inst : Nontrivial β
h : Eq.{u_2 + 1} (α := α) 1 0
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
rw₁ rw₂ : Eq.{u_3 + 1} (α := β) 0 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
h : Subsingleton α
⊢ Subsingleton β

Tactic:
(subsingleton_or_nontrivial β).resolve_right fun _ =>
    not_nontrivial_iff_subsingleton.mpr h f.domain_nontrivial

Premises used: Iff.mpr, not_nontrivial_iff_subsingleton, subsingleton_or_nontrivial, RingHom.domain_nontrivial, Or.resolve_right
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonAssocRing α
inst_1 : NonAssocRing β
f : α →+* β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (-x) : β) (-(f : (a : α) → β) x : β)

Tactic:
map_neg f x

Premises used: map_neg
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : NonAssocRing α
inst_1 : NonAssocRing β
f : α →+* β
x y : α
⊢ (f : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
map_sub f x y

Premises used: map_sub
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
x : NonAssocSemiring α
⊢ Eq (α := (a : α) → α) (⇑(id α) : (a : α) → α) _root_.id

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
x : NonAssocSemiring α
⊢ Eq (α := α →* α) (↑(id α) : α →* α) (MonoidHom.id α)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
g : β →+* γ
f : α →+* β
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f : (a : α) → β) 1 : β) : γ) (1 : γ)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
δ : Type u_5
x_3 : NonAssocSemiring δ
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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
hnp : β →+* γ
hmn : α →+* β
⊢ Eq (α := (a : α) → γ) (⇑(hnp.comp hmn) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
x_3 : NonAssocSemiring γ
hnp : β →+* γ
hmn : α →+* β
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((hnp.comp hmn : (a : α) → γ) x : γ) ((hnp : (a : β) → γ) ((hmn : (a : α) → β) x : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ f.comp (id α) = f

Tactic:
ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ comp (id β) f = f

Tactic:
ext fun _ => rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

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
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
n : ℕ
f : α →+* α
zero : Eq (α := α → α) (⇑f : (a : α) → α)^[0] (⇑(npowRec 0 f) : (a : α) → α)
succ :
  ∀ (n : ℕ),
    Eq (α := α → α) (⇑f : (a : α) → α)^[n] (⇑(npowRec n f) : (a : α) → α) →
      Eq (α := α → α) (⇑f : (a : α) → α)^[n + 1] (⇑(npowRec (n + 1) f) : (a : α) → α)
⊢ Eq (α := α → α) (⇑f : (a : α) → α)^[n] (⇑(npowRec n f) : (a : α) → α)

Tactic:
induction n
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
f : α →+* α
⊢ Eq (α := α → α) (⇑f : (a : α) → α)^[0] (⇑(npowRec 0 f) : (a : α) → α)

Tactic:
simp [npowRec, *]

Premises used: npowRec
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
f : α →+* α
n : ℕ
h : Eq (α := α → α) (⇑f : (a : α) → α)^[n] (⇑(npowRec n f) : (a : α) → α)
⊢ Eq (α := α → α) (⇑f : (a : α) → α)^[n + 1] (⇑(npowRec (n + 1) f) : (a : α) → α)

Tactic:
simp [npowRec, *]

Premises used: npowRec
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
x : NonAssocSemiring α
f : α →+* α
n : ℕ
⊢ Eq (α := (a : α) → α) (⇑(f ^ n) : (a : α) → α) (⇑f : (a : α) → α)^[n]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
g₁ g₂ : β →+* γ
f : α →+* β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => RingHom.ext <| hf.forall.2 (RingHom.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, RingHom.ext_iff, Eq.rec, RingHom.ext, Iff.intro, Iff.mp, rfl