awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star 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
h₆ :
  ∀ (x : A),
    (↑(↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ :
                      A →ₐ[R] B }.toRingHom :
                A →* B) :
            OneHom A B).toFun
        (star x) =
      star
        ((↑(↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ :
                        A →ₐ[R] B }.toRingHom :
                  A →* B) :
              OneHom A B).toFun
          x)
⊢ (⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ :
          A →⋆ₐ[R] B } :
      (a : A) → B) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
f : A →ₐ[R] B
h :
  ∀ (x : A),
    (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun (star x) = star ((↑(↑f.toRingHom : A →* B) : OneHom A B).toFun x)
⊢ Eq (α := (a : A) → B) (⇑{ toAlgHom := f, map_star' := h : A →⋆ₐ[R] B } : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
f : A →⋆ₐ[R] B
h₁ : Eq.{u_4 + 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
h₆ :
  ∀ (x : A),
    (↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                      commutes' := h₅ : A →ₐ[R] B }.toRingHom :
                A →* B) :
            OneHom A B).toFun
        (star x) =
      star
        ((↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                        commutes' := h₅ : A →ₐ[R] B }.toRingHom :
                  A →* B) :
              OneHom A B).toFun
          x)
h :
  ∀ (x : A),
    Eq.{u_4 + 1} (α := B)
      (({ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅,
              map_star' := h₆ : A →⋆ₐ[R] B } :
            (a : A) → B)
          x :
        B)
      ((f : (a : A) → B) x : B)
⊢ { toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅,
      map_star' := h₆ : A →⋆ₐ[R] B } =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
f : A →⋆ₐ[R] B
h₁ : Eq.{u_4 + 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
h₆ :
  ∀ (x : A),
    (↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                      commutes' := h₅ : A →ₐ[R] B }.toRingHom :
                A →* B) :
            OneHom A B).toFun
        (star x) =
      star
        ((↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                        commutes' := h₅ : A →ₐ[R] B }.toRingHom :
                  A →* B) :
              OneHom A B).toFun
          x)
x : A
⊢ Eq.{u_4 + 1} (α := B)
    (({ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅,
            map_star' := h₆ : A →⋆ₐ[R] B } :
          (a : A) → B)
        x :
      B)
    ((f : (a : A) → B) x : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
⊢ Eq (α := (a : A) → A) (⇑(StarAlgHom.id R A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R_1 : Type u_2
A_1 : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : Star A_1
inst_4 : Semiring B
inst_5 : Algebra R_1 B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R_1 C
inst_9 : Star C
inst_10 : Semiring D
inst_11 : Algebra R_1 D
inst_12 : Star D
R : Type u_7
A : Type u_8
inst_13 : CommSemiring R
inst_14 : StarRing R
inst_15 : Semiring A
inst_16 : StarMul A
inst_17 : Algebra R A
inst_18 : StarModule R A
⊢ ∀ (x : R),
    Eq.{u_8 + 1} (α := A) ((algebraMap R A : (a : R) → A) (star x) : A) (star ((algebraMap R A : (a : R) → A) x) : A)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
inst_10 : Semiring D
inst_11 : Algebra R D
inst_12 : Star D
f : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
⊢ ∀ (x : A),
    (↑(↑((↑f : B →ₐ[R] C).comp (↑g : A →ₐ[R] B)).toRingHom : A →* C) : OneHom A C).toFun (star x) =
      star ((↑(↑((↑f : B →ₐ[R] C).comp (↑g : A →ₐ[R] B)).toRingHom : A →* C) : OneHom A C).toFun x)

Tactic:
simp only [map_star, AlgHom.toFun_eq_coe, AlgHom.coe_comp, coe_toAlgHom,
        Function.comp_apply, forall_const]

Premises used: StarHomClass.map_star, StarAlgHom.coe_toAlgHom, AlgHom.coe_comp, forall_const, Function.comp_apply, AlgHom.toFun_eq_coe
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
⊢ Eq (α := (a : A) → C) (⇑(f.comp g) : (a : A) → C)
    (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := B) (⇑f : (a : B) → C) (⇑g : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
a : A
⊢ Eq.{u_5 + 1} (α := C) ((f.comp g : (a : A) → C) a : C) ((f : (a : B) → C) ((g : (a : A) → B) a : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
inst_10 : Semiring D
inst_11 : Algebra R D
inst_12 : Star D
f : C →⋆ₐ[R] D
g : B →⋆ₐ[R] C
h : A →⋆ₐ[R] B
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: StarAlgHom.comp, AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
f : A →⋆ₐ[R] B
⊢ comp (StarAlgHom.id R B) f = f

Tactic:
ext fun _ => rfl

Premises used: StarAlgHom.ext, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
f : A →⋆ₐ[R] B
⊢ f.comp (StarAlgHom.id R A) = f

Tactic:
ext fun _ => rfl

Premises used: StarAlgHom.ext, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
f : A →⋆ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑f.toNonUnitalStarAlgHom : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x : A
⊢ (f.prod g.toNonUnitalAlgHom).toFun (star x) = star ((f.prod g.toNonUnitalAlgHom).toFun x)

Tactic:
simp [map_star, Prod.ext_iff]

Premises used: Prod.ext_iff, StarHomClass.map_star
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ Eq (α := (a : A) → B × C) (⇑(f.prod g) : (a : A) → B × C)
    (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
⊢ comp (fst R B C) (f.prod g) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x : A
⊢ Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
h : ∀ (x : A), Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
⊢ comp (snd R B C) (f.prod g) = g

Tactic:
ext
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x : A
⊢ Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
⊢ Eq (α := A × B →⋆ₙₐ[R] A × B) (prod (fst R A B) (snd R A B)) 1

Tactic:
DFunLike.coe_injective Function.prod_fst_snd

Premises used: Function.prod_fst_snd, DFunLike.coe_injective
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : StarAddMonoid A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : StarAddMonoid B
⊢ Eq (α := (a : A) → A × B) (⇑(inl R A B) : (a : A) → A × B) fun (x : A) ↦ (x, 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : StarAddMonoid A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : StarAddMonoid B
x : A
⊢ Eq (α := A × B) ((inl R A B : (a : A) → A × B) x : A × B) ((x, 0) : A × B)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : StarAddMonoid A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : StarAddMonoid B
⊢ Eq (α := (a : B) → A × B) (⇑(inr R A B) : (a : B) → A × B) (Prod.mk 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : StarAddMonoid A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : StarAddMonoid B
x : B
⊢ Eq (α := A × B) ((inr R A B : (a : B) → A × B) x : A × B) ((0, x) : A × B)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x : A
⊢ (↑(↑((↑f : A →ₐ[R] B).prod (↑g : A →ₐ[R] C)).toRingHom : A →* B × C) : OneHom A (B × C)).toFun (star x) =
    star ((↑(↑((↑f : A →ₐ[R] B).prod (↑g : A →ₐ[R] C)).toRingHom : A →* B × C) : OneHom A (B × C)).toFun x)

Tactic:
simp [Prod.star_def, map_star]

Premises used: StarHomClass.map_star, Prod.star_def
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ Eq (α := (a : A) → B × C) (⇑(f.prod g) : (a : A) → B × C)
    (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
⊢ comp (fst R B C) (f.prod g) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x : A
⊢ Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
h : ∀ (x : A), Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
⊢ comp (snd R B C) (f.prod g) = g

Tactic:
ext
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x : A
⊢ Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
⊢ Eq (α := A × B →⋆ₐ[R] A × B) (prod (fst R A B) (snd R A B)) 1

Tactic:
DFunLike.coe_injective Function.prod_fst_snd

Premises used: Function.prod_fst_snd, DFunLike.coe_injective
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : DistribMulAction R B
inst_5 : EquivLike F A B
inst_6 : NonUnitalAlgEquivClass F R A B
⊢ NonUnitalAlgHomClass F R A B

Tactic:

Premises used: NonUnitalAlgSemiHomClass.mk
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : EquivLike F A B
inst_6 : NonUnitalAlgEquivClass F R A B
f : F
r : R
⊢ Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)

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

Premises used: Algebra.algebraMap_eq_smul_one, map_one, map_smul
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : SMul R A
inst_5 : SMul R B
inst_6 : Star A
inst_7 : Star B
inst_8 : Add C
inst_9 : Mul C
inst_10 : SMul R C
inst_11 : Star C
f g : A ≃⋆ₐ[R] B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
rcases :
  ∀ (toFun : A → B) (invFun : B → A) (left_inv : Function.LeftInverse invFun toFun)
    (right_inv : Function.RightInverse invFun toFun)
    (map_mul' :
      ∀ (x y : A),
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun (x * y) =
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun x *
            { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun y)
    (map_add' :
      ∀ (x y : A),
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun (x + y) =
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun x +
            { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun y)
    (map_star' :
      ∀ (a : A),
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                map_add' := map_add' : A ≃+* B }.toFun
            (star a) =
          star
            ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                  map_add' := map_add' : A ≃+* B }.toFun
              a))
    (map_smul' :
      ∀ (r : R) (a : A),
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                map_add' := map_add', map_star' := map_star' : A ≃⋆+* B }.toFun
            (r • a) =
          r •
            { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                  map_add' := map_add', map_star' := map_star' : A ≃⋆+* B }.toFun
              a)
    (h₁ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
            map_add' := map_add', map_star' := map_star', map_smul' := map_smul' : A ≃⋆ₐ[R] B }.toFun =
        g.toFun)
    (h₂ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
            map_add' := map_add', map_star' := map_star', map_smul' := map_smul' : A ≃⋆ₐ[R] B }.invFun =
        g.invFun),
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
        map_add' := map_add', map_star' := map_star', map_smul' := map_smul' : A ≃⋆ₐ[R] B } =
      g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨⟨_, _, _⟩, _⟩, _⟩, _⟩
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : SMul R A
inst_5 : SMul R B
inst_6 : Star A
inst_7 : Star B
e : A ≃⋆ₐ[R] B
⊢ e.toStarRingEquiv = (↑e : A ≃⋆+* B)

Tactic:
rfl

Premises used: StarRingEquivClass.toStarRingEquiv, RingEquivClass.toRingEquiv, EquivLike.toEquiv, rfl