awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
f g : A →ₐ[R] B
h :
  Eq (α := (a : A) → B) ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) f)
    ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
rcases :
  ∀ (toFun : A → B) (map_one' : toFun 1 = 1)
    (map_mul' :
      ∀ (x y : A),
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
          { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
            { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y)
    (map_zero' : (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun 0 = 0)
    (map_add' :
      ∀ (x y : A),
        (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun (x + y) =
          (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun x +
            (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun y)
    (commutes' :
      ∀ (r : R),
        (↑(↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                        A →+* B } :
                    A →* B) :
                OneHom A B).toFun
            ((algebraMap R A : (a : R) → A) r) =
          (algebraMap R B : (a : R) → B) r)
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
          { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
            commutes' := commutes' })
        ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)),
    { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
        commutes' := commutes' : A →ₐ[R] B } =
      g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
⊢ Eq (α := A →ₗ[R] B)
    (↑(↑f : A →ₐ[R] B) :
      [inst_7 : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)
    (↑f : [inst_7 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, AlgHomClass.toAlgHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
F : Type u_1
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₐ[R] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun = (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →+* B
h : ∀ (r : R), (↑(↑f : A →* B) : OneHom A B).toFun ((algebraMap R A : (a : R) → A) r) = (algebraMap R B : (a : R) → B) r
⊢ Eq (α := (a : A) → B) (⇑{ toRingHom := f, commutes' := h : A →ₐ[R] B } : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A → B
h₁ : f 1 = 1
h₂ :
  ∀ (x y : A),
    { toFun := f, map_one' := h₁ : OneHom A B }.toFun (x * y) =
      { toFun := f, map_one' := h₁ : OneHom A B }.toFun x * { toFun := f, map_one' := h₁ : OneHom A B }.toFun y
h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun y
h₅ :
  ∀ (r : R),
    (↑(↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ : A →+* B } : A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
⊢ (⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ : A →ₐ[R] B } :
      (a : A) → B) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →+* B
h : ∀ (r : R), (↑(↑f : A →* B) : OneHom A B).toFun ((algebraMap R A : (a : R) → A) r) = (algebraMap R B : (a : R) → B) r
⊢ (↑{ toRingHom := f, commutes' := h : A →ₐ[R] B } : A →+* B) = f

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ f.toRingHom = (↑f : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →+* B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →* B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →+ B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := A →* B) (↑(↑f : A →+* B) : A →* B) (↑f : A →* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := A →+ B) (↑(↑f : A →+* B) : A →+ B) (↑f : A →+ B)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Injective (α := A →ₐ[R] B) (β := A → B) (DFunLike.coe (β := fun (x : A) ↦ B))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ₁ φ₂ : A →ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑φ₁ : (a : A) → B) (⇑φ₂ : (a : A) → B) ↔ φ₁ = φ₂

Tactic:
DFunLike.coe_fn_eq

Premises used: DFunLike.coe_fn_eq
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Injective (α := A →ₐ[R] B) (β := A →+* B) RingHomClass.toRingHom

Tactic:
fun φ₁ φ₂ H =>
  coe_fn_injective <| show ((φ₁ : A →+* B) : A → B) = ((φ₂ : A →+* B) : A → B) from congr_arg _ H

Premises used: congr_arg, AlgHom.coe_fn_injective, Function.Injective, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Injective (α := A →ₐ[R] B) (β := A →* B) MonoidHomClass.toMonoidHom

Tactic:
RingHom.coe_monoidHom_injective.comp coe_ringHom_injective

Premises used: AlgHom.coe_ringHom_injective, MonoidHomClass.toMonoidHom, Function.Injective.comp, RingHom.coe_monoidHom_injective
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Injective (α := A →ₐ[R] B) (β := A →+ B) AddMonoidHomClass.toAddMonoidHom

Tactic:
RingHom.coe_addMonoidHom_injective.comp coe_ringHom_injective

Premises used: AlgHom.coe_ringHom_injective, AddMonoidHomClass.toAddMonoidHom, Function.Injective.comp, RingHom.coe_addMonoidHom_injective
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ₁ φ₂ : A →ₐ[R] B
H : φ₁ = φ₂
x : A
⊢ Eq.{w + 1} (α := B) ((φ₁ : (a : A) → B) x : B) ((φ₂ : (a : A) → B) x : B)

Tactic:
DFunLike.congr_fun H x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
x y : A
h : x = y
⊢ Eq.{w + 1} (α := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) y : B)

Tactic:
DFunLike.congr_arg φ h

Premises used: DFunLike.congr_arg
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ₁ φ₂ : A →ₐ[R] B
H : ∀ (x : A), Eq.{w + 1} (α := B) ((φ₁ : (a : A) → B) x : B) ((φ₂ : (a : A) → B) x : B)
⊢ φ₁ = φ₂

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
h₁ : Eq.{w + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
h₂ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun y
h₃ : (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun y
h₅ :
  ∀ (r : R),
    (↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ : A →+* B } :
                A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
⊢ { toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ :
      A →ₐ[R] B } =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := A →ₙ+ B) { toFun := (⇑f : (a : A) → B), map_add' := ⋯ } (↑f : A →ₙ+ B)

Tactic:
rfl

Premises used: AddHomClass.toAddHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
r : R
⊢ Eq.{w + 1} (α := B) ((φ : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
φ.commutes' r

Premises used: AlgHom.commutes'
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
⊢ Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑φ : A →+* B) (algebraMap R A))
    (algebraMap R B)

Tactic:
RingHom.ext <| φ.commutes

Premises used: RingHom.ext, AlgHom.commutes
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
φ : A →ₐ[R] B
f : A →+* B
h : ∀ (c : R) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : R
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) c : A) : B)
    ((algebraMap R B : (a : R) → B) c : B)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, h, f.map_one]

Premises used: RingHom.map_one, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →+* B
h : ∀ (c : R) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
⊢ Eq (α := (a : A) → B) (⇑(mk' f h) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := (a : A) → A) (⇑(AlgHom.id R A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := A →+* A) (↑(AlgHom.id R A) : A →+* A) (RingHom.id A)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : A
⊢ (AlgHom.id R A : (a : A) → A) p = p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
rw :
  OneHom.toFun (↑(↑(φ₁.comp (↑φ₂ : A →+* B)) : A →* C) : OneHom A C) ((algebraMap R A : (a : R) → A) r) =
    (φ₁ : (a : B) → C) ((φ₂ : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
⊢ OneHom.toFun (↑(↑(φ₁.comp (↑φ₂ : A →+* B)) : A →* C) : OneHom A C) ((algebraMap R A : (a : R) → A) r) =
    (algebraMap R C : (a : R) → C) r

Tactic:
rw [← φ₁.commutes, ← φ₂.commutes]

Premises used: AlgHom.commutes
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
⊢ OneHom.toFun (↑(↑(φ₁.comp (↑φ₂ : A →+* B)) : A →* C) : OneHom A C) ((algebraMap R A : (a : R) → A) r) =
    (φ₁ : (a : B) → C) ((φ₂ : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
⊢ Eq (α := (a : A) → C) (⇑(φ₁.comp φ₂) : (a : A) → C)
    (Function.comp.{v + 1, w + 1, u₁ + 1} (β := B) (⇑φ₁ : (a : B) → C) (⇑φ₂ : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
p : A
⊢ Eq.{u₁ + 1} (α := C) ((φ₁.comp φ₂ : (a : A) → C) p : C) ((φ₁ : (a : B) → C) ((φ₂ : (a : A) → B) p : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
⊢ Eq (α := A →+* C) (↑(φ₁.comp φ₂) : A →+* C)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑φ₁ : B →+* C) (↑φ₂ : A →+* B))

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
⊢ φ.comp (AlgHom.id R A) = φ

Tactic:
rfl

Premises used: AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
⊢ comp (AlgHom.id R B) φ = φ

Tactic:
rfl

Premises used: AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
φ₁ : C →ₐ[R] D
φ₂ : B →ₐ[R] C
φ₃ : A →ₐ[R] B
⊢ (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)

Tactic:
rfl

Premises used: AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
⊢ RingHomCompTriple φ₂.toRingHom φ₁.toRingHom (φ₁.comp φ₂).toRingHom

Tactic:
⟨rfl⟩

Premises used: RingHomCompTriple.mk, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
p : A
⊢ Eq.{w + 1} (α := B) ((φ.toLinearMap : (a : A) → B) p : B) ((φ : (a : A) → B) p : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑φ.toLinearMap : (a : A) → B) (⇑φ : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Injective (α := A →ₐ[R] B) toLinearMap

Tactic:
fun _φ₁ _φ₂ h =>
  ext <| LinearMap.congr_fun h

Premises used: AlgHom.ext, LinearMap.congr_fun, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
⊢ (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := A →ₗ[R] A) (toLinearMap (AlgHom.id R A)) LinearMap.id

Tactic:
rfl

Premises used: AlgHom.toLinearMap, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ { toAddHom := (↑f : A →ₙ+ B), map_smul' := ⋯ } = f.toLinearMap

Tactic:
rfl

Premises used: AlgHom.toLinearMap, AddHomClass.toAddHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
φ : A →ₐ[R] B
f : A →ₗ[R] B
map_one : Eq.{w + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
map_mul :
  ∀ (x y : A),
    (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
c : R
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) c : A) : B)
    ((algebraMap R B : (a : R) → B) c : B)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, f.map_smul, map_one]

Premises used: Algebra.algebraMap_eq_smul_one, LinearMap.map_smul
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
map_one : Eq.{w + 1} (α := B) ((φ.toLinearMap : (a : A) → B) 1 : B) (1 : B)
map_mul :
  ∀ (x y : A),
    (φ.toLinearMap : (a : A) → B) (x * y) =
      HMul.hMul (α := B) (β := B) ((φ.toLinearMap : (a : A) → B) x : B) ((φ.toLinearMap : (a : A) → B) y : B)
⊢ ofLinearMap φ.toLinearMap map_one map_mul = φ

Tactic:
rfl

Premises used: AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
map_one : Eq.{w + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
map_mul :
  ∀ (x y : A),
    (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ (ofLinearMap f map_one map_mul).toLinearMap = f

Tactic:
rfl

Premises used: AlgHom.toLinearMap, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
map_one : Eq.{v + 1} (α := A) ((LinearMap.id : (a : A) → A) 1 : A) (1 : A)
map_mul :
  ∀ (x y : A),
    (LinearMap.id : (a : A) → A) (x * y) =
      HMul.hMul (α := A) (β := A) ((LinearMap.id : (a : A) → A) x : A) ((LinearMap.id : (a : A) → A) y : A)
⊢ ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A

Tactic:
rfl

Premises used: AlgHom.ofLinearMap, AlgHom.id, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ : A →ₐ[R] B
R' : Type u_1
inst_5 : SMul R' A
inst_6 : SMul R' B
inst_7 : LinearMap.CompatibleSMul A B R' R
r : R'
x : A
⊢ (φ : (a : A) → B) (r • x) = HSMul.hSMul (β := B) r ((φ : (a : A) → B) x : B)

Tactic:
φ.toLinearMap.map_smul_of_tower r x

Premises used: AlgHom.toLinearMap, LinearMap.map_smul_of_tower
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ (1 : (a : A) → A) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ ψ : A →ₐ[R] A
x : A
⊢ Eq (α := A) ((φ * ψ : (a : A) → A) x : A) ((φ : (a : A) → A) ((ψ : (a : A) → A) x : A) : A)

Tactic:
rfl

Premises used: rfl