awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R_1 : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Star R
inst_2 : Mul S
inst_3 : Star S
inst_4 : FunLike F R S
inst_5 : MulHomClass F R S
inst_6 : StarHomClass F R S
f : F
r : R
hr : IsStarNormal r
⊢ Commute.{u_5} (S := S) (star ((f : (a : R) → S) r) : S) ((f : (a : R) → S) r : S)

Tactic:
simpa [map_star] using congr(f $(hr.star_comm_self))

Premises used: StarHomClass.map_star
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : StarMul R
inst_2 : TrivialStar R
x : R
rw rw₁ : Commute x x
⊢ Commute (star x) x

Tactic:
rw [star_trivial]

Premises used: TrivialStar.star_trivial
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : CommMonoid R
inst_1 : StarMul R
x : R
⊢ IsStarNormal x

Tactic:
⟨mul_comm _ _⟩

Premises used: IsStarNormal.mk, mul_comm
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : IsStarNormal a
hb : IsStarNormal b
rw : ∀ (ha : Commute (star a) a) (hb : Commute (star b) b), Commute (star (a + b)) (a + b)
⊢ IsStarNormal (a + b)

Tactic:
rw [isStarNormal_iff] at ha hb ⊢

Premises used: isStarNormal_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
⊢ Commute (star a) b

Tactic:
have := _root_.star_star b ▸ hab.star_star
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
simp : star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
⊢ Commute (star (a + b)) (a + b)

Tactic:
simp only [star_add, commute_iff_eq, mul_add, add_mul]

Premises used: add_mul, StarAddMonoid.star_add, commute_iff_eq, mul_add
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
rw : a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
rw₁ : a * star a + star b * a + (star a * b + b * star b) = a * star a + b * star a + (a * star b + b * star b)
rw₂ : a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (a * star b + b * star b)
rw₃ : a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (star b * a + b * star b)
rw₄ rw₅ : a * star a + b * star a + (star b * a + b * star b) = a * star a + b * star a + (star b * a + b * star b)
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)

Tactic:
rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]

Premises used: add_add_add_comm, Commute.eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : IsStarNormal a
hb : IsStarNormal b
⊢ IsStarNormal (a - b)

Tactic:
sub_eq_add_neg a b ▸ (star_neg b ▸ hab.neg_right).isStarNormal_add

Premises used: sub_eq_add_neg, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : StarRing R
a : R
ha : IsStarNormal a
⊢ IsStarNormal (1 + a)

Tactic:
Commute.one_left (star a) |>.isStarNormal_add

Premises used: Commute.isStarNormal_add, Star.star, Commute.one_left
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocRing R
inst_1 : StarRing R
a : R
ha : IsStarNormal a
⊢ IsStarNormal (1 - a)

Tactic:
Commute.one_left (star a) |>.isStarNormal_sub

Premises used: Commute.isStarNormal_sub, Star.star, Commute.one_left
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ b * a = 0

Tactic:
simpa [ha.star_eq, hb.star_eq] using congr(star $hab)

Premises used: IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ b * a = 0

Tactic:
have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
this : b * a = 0
⊢ Commute a b

Tactic:
grind [commute_iff_eq]

Premises used: commute_iff_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Star (α i)
f : (i : ι) → α i
⊢ IsSelfAdjoint f ↔ ∀ (i : ι), IsSelfAdjoint (f i)

Tactic:
funext_iff

Premises used: IsSelfAdjoint, funext_iff
-- 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 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
⊢ NonUnitalStarRingHomClass F A B

Tactic:
NonUnitalStarRingHomClass.mk

Premises used: NonUnitalStarRingHomClass.mk
-- 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
F : Type u_6
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F 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.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
f : A →⋆ₙₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑f.toNonUnitalAlgHom : (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
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
f g : A →⋆ₙₐ[R] B
h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- 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
f : A →⋆ₙₐ[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (⇑(f.copy f' h) : (a : A) → B) = f'

Tactic:
rfl

Premises used: 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
f : A →⋆ₙₐ[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- 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
f : A → B
h₁ : ∀ (m : R) (x : A), f (m • x) = HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) m : R) (f x)
h₂ : { toFun := f, map_smul' := h₁ : MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := f, map_smul' := h₁ : MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
        (x + y) =
      { toFun := f, map_smul' := h₁ : MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun x +
        { toFun := f, map_smul' := h₁ : MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun (x * y) =
      { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun x *
        { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₙₐ[R] B }.toFun (star a) =
      star ({ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₙₐ[R] B }.toFun a)
⊢ (⇑{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := 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_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
f : A →ₙₐ[R] B
h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)
⊢ Eq (α := (a : A) → B) (⇑{ toNonUnitalAlgHom := 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_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
f : A →⋆ₙₐ[R] B
h₁ :
  ∀ (m : R) (x : A),
    (f : (a : A) → B) (m • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) m : R) ((f : (a : A) → B) x : B)
h₂ :
  { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
          MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
      0 =
    0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
            MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
        (x + y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          x +
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          y
h₄ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₙₐ[R] B }.toFun
        (star a) =
      star
        ({ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ :
              A →ₙₐ[R] B }.toFun
          a)
h :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := B)
      (({ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄,
              map_star' := h₅ : A →⋆ₙₐ[R] B } :
            (a : A) → B)
          x :
        B)
      ((f : (a : A) → B) x : B)
⊢ { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ :
      A →⋆ₙₐ[R] B } =
    f

Tactic:
ext
-- 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
f : A →⋆ₙₐ[R] B
h₁ :
  ∀ (m : R) (x : A),
    (f : (a : A) → B) (m • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) m : R) ((f : (a : A) → B) x : B)
h₂ :
  { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
          MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
      0 =
    0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
            MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
        (x + y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          x +
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          y
h₄ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₙₐ[R] B }.toFun
        (star a) =
      star
        ({ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ :
              A →ₙₐ[R] B }.toFun
          a)
x : A
⊢ Eq.{u_3 + 1} (α := B)
    (({ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := 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_1
A : Type u_2
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
⊢ Eq (α := (a : A) → A) (⇑(NonUnitalStarAlgHom.id R A) : (a : A) → A) id

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
D : Type u_5
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
inst_10 : NonUnitalNonAssocSemiring D
inst_11 : DistribMulAction R D
inst_12 : Star D
f : B →⋆ₙₐ[R] C
g : A →⋆ₙₐ[R] B
⊢ ∀ (a : A), (f.comp g.toNonUnitalAlgHom).toFun (star a) = star ((f.comp g.toNonUnitalAlgHom).toFun a)

Tactic:
simp only [map_star, NonUnitalAlgHom.toFun_eq_coe, NonUnitalAlgHom.coe_comp,
        coe_toNonUnitalAlgHom, Function.comp_apply, forall_const]

Premises used: StarHomClass.map_star, NonUnitalAlgHom.coe_comp, NonUnitalStarAlgHom.coe_toNonUnitalAlgHom, NonUnitalAlgHom.toFun_eq_coe, forall_const, Function.comp_apply
-- 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 : B →⋆ₙₐ[R] C
g : A →⋆ₙₐ[R] B
⊢ Eq (α := (a : A) → C) (⇑(f.comp g) : (a : A) → C)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := B) (⇑f : (a : B) → C) (⇑g : (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 : B →⋆ₙₐ[R] C
g : A →⋆ₙₐ[R] B
a : A
⊢ Eq.{u_4 + 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_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
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
inst_10 : NonUnitalNonAssocSemiring D
inst_11 : DistribMulAction 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: NonUnitalAlgHom.comp, NonUnitalStarAlgHom.comp, 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
f : A →⋆ₙₐ[R] B
⊢ comp (NonUnitalStarAlgHom.id R B) f = f

Tactic:
ext fun _ => rfl

Premises used: rfl, NonUnitalStarAlgHom.ext
-- 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
f : A →⋆ₙₐ[R] B
⊢ f.comp (NonUnitalStarAlgHom.id R A) = f

Tactic:
ext fun _ => rfl

Premises used: rfl, NonUnitalStarAlgHom.ext
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
⊢ Eq.{u_2 + 1} (α := (a : A) → A) (⇑1 : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
a : A
⊢ (1 : (a : A) → A) a = a

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
D : Type u_5
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
⊢ ∀ (a : A),
    Eq.{u_3 + 1} (α := B)
      (MulActionHom.toFun.{u_1, u_1, u_2, u_3} (M := R) (N := R) (φ := (⇑(MonoidHom.id R) : (a : R) → R))
        (DistribMulActionHom.toMulActionHom (NonUnitalAlgHom.toDistribMulActionHom 0)) (star a))
      (star
        (MulActionHom.toFun.{u_1, u_1, u_2, u_3} (M := R) (N := R) (φ := (⇑(MonoidHom.id R) : (a : R) → R))
          (DistribMulActionHom.toMulActionHom (NonUnitalAlgHom.toDistribMulActionHom 0)) a))

Tactic:
simp
-- 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) → B) (⇑0 : (a : A) → B) 0

Tactic:
rfl

Premises used: 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
a : A
⊢ Eq.{u_3 + 1} (α := B) ((0 : (a : A) → B) a : B) (0 : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : Star A
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : MulAction R S
inst_7 : DistribMulAction S A
inst_8 : DistribMulAction S B
inst_9 : DistribMulAction R A
inst_10 : DistribMulAction R B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →⋆ₙₐ[S] B
x : A
⊢ Eq.{u_4 + 1} (α := B) ((restrictScalars R f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : Star A
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : MulAction R S
inst_7 : DistribMulAction S A
inst_8 : DistribMulAction S B
inst_9 : DistribMulAction R A
inst_10 : DistribMulAction R B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →⋆ₙₐ[S] B
⊢ Eq (α := A →ₙ+* B) (↑(restrictScalars R f) : A →ₙ+* B) (↑f : A →ₙ+* B)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, NonUnitalStarAlgHom.restrictScalars, NonUnitalRingHomClass.toNonUnitalRingHom, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : Star A
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : MulAction R S
inst_7 : DistribMulAction S A
inst_8 : DistribMulAction S B
inst_9 : DistribMulAction R A
inst_10 : DistribMulAction R B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →⋆ₙₐ[S] B
⊢ Eq (α := (a : A) → B) (⇑(restrictScalars R f) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : Star A
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : MulAction R S
inst_7 : DistribMulAction S A
inst_8 : DistribMulAction S B
inst_9 : DistribMulAction R A
inst_10 : DistribMulAction R B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
⊢ Function.Injective (α := A →⋆ₙₐ[S] B) (β := A →⋆ₙₐ[R] B) (restrictScalars R)

Tactic:
fun _ _ h ↦ ext (DFunLike.congr_fun h :)

Premises used: DFunLike.congr_fun, Function.Injective, NonUnitalStarAlgHom.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 : Type u_7
inst_7 : FunLike F A B
inst_8 : AlgHomClass F R A B
inst_9 : StarHomClass F 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.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 : 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 g : A →⋆ₐ[R] B
h : ∀ (x : A), Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.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
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (⇑(f.copy f' h) : (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
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'