awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(skewAdjoint A)
hr :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              0 :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              x :
            A) -
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                0 :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                x :
              A))) =
    (↑x : A)
⊢ Eq.{u_2 + 1} (α := A)
    (↑((((LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
                      LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                        (Submodule.subtype (skewAdjoint.submodule R A)) :
                    ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) ∘ₗ
                  (LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                    ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
              (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).2 :
      A)
    (↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A) :
              (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).2 :
      A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(selfAdjoint A)
hl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑x : A) + (↑0 : A) + star ((↑x : A) + (↑0 : A))) =
    (↑x : A)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              x :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              0 :
            A) +
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                x :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                0 :
              A))) =
    (↑x : A)

Tactic:
erw [Submodule.coe_subtype, Submodule.coe_subtype]

Premises used: Submodule.coe_subtype
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(selfAdjoint A)
hl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑x : A) + (↑0 : A) - star ((↑x : A) + (↑0 : A))) =
    0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              x :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              0 :
            A) -
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                x :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                0 :
              A))) =
    0

Tactic:
erw [Submodule.coe_subtype, Submodule.coe_subtype]

Premises used: Submodule.coe_subtype
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(skewAdjoint A)
hr :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑0 : A) + (↑x : A) + star ((↑0 : A) + (↑x : A))) =
    0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              0 :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              x :
            A) +
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                0 :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                x :
              A))) =
    0

Tactic:
erw [Submodule.coe_subtype, Submodule.coe_subtype]

Premises used: Submodule.coe_subtype
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(skewAdjoint A)
hr :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑0 : A) + (↑x : A) - star ((↑0 : A) + (↑x : A))) =
    (↑x : A)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              0 :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              x :
            A) -
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                0 :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                x :
              A))) =
    (↑x : A)

Tactic:
erw [Submodule.coe_subtype, Submodule.coe_subtype]

Premises used: Submodule.coe_subtype
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(selfAdjoint A)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑x : A) + (↑0 : A) + star ((↑x : A) + (↑0 : A))) =
    (↑x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(selfAdjoint A)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑x : A) + (↑0 : A) - star ((↑x : A) + (↑0 : A))) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(skewAdjoint A)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑0 : A) + (↑x : A) + star ((↑0 : A) + (↑x : A))) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(skewAdjoint A)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((↑0 : A) + (↑x : A) - star ((↑0 : A) + (↑x : A))) =
    (↑x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarMul A
inst_4 : Algebra R A
inst_5 : StarModule R A
r : R
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) (star r) : A) (star ((algebraMap R A : (a : R) → A) r) : A)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, star_smul, star_one]

Premises used: StarModule.star_smul, Algebra.algebraMap_eq_smul_one, star_one
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarMul A
inst_4 : Algebra R A
inst_5 : StarModule R A
r : R
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint.{u_2} (R := A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
simpa using congr(algebraMap R A $(hr.star_eq))
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarMul A
inst_4 : Algebra R A
inst_5 : StarModule R A
r : R
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ IsSelfAdjoint.{u_2} (R := A) ((algebraMap R A : (a : R) → A) r : A) ↔ IsSelfAdjoint r

Tactic:
⟨fun hr ↦ h <| algebraMap_star_comm r (A := A) ▸ hr.star_eq, IsSelfAdjoint.algebraMap A⟩

Premises used: Eq.rec, IsSelfAdjoint.algebraMap, Iff.intro, Eq.symm, IsSelfAdjoint.star_eq, algebraMap_star_comm
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
⊢ IsIdempotentElem (star a) ↔ IsIdempotentElem a

Tactic:
simp [IsIdempotentElem, ← star_mul]

Premises used: IsIdempotentElem, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f g : A →⋆* B
h :
  Eq (α := (a : A) → B) ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) f)
    ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) g)
mk :
  ∀ (toMonoidHom : A →* B)
    (map_star' : ∀ (a : A), (↑toMonoidHom : OneHom A B).toFun (star a) = star ((↑toMonoidHom : OneHom A B).toFun a))
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
          { toMonoidHom := toMonoidHom, map_star' := map_star' })
        ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) g)),
    { toMonoidHom := toMonoidHom, map_star' := map_star' : A →⋆* B } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
g : A →⋆* B
toMonoidHom : A →* B
map_star' : ∀ (a : A), (↑toMonoidHom : OneHom A B).toFun (star a) = star ((↑toMonoidHom : OneHom A B).toFun a)
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) { toMonoidHom := toMonoidHom, map_star' := map_star' })
    ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) g)
mk :
  ∀ (toMonoidHom_1 : A →* B)
    (map_star'_1 :
      ∀ (a : A), (↑toMonoidHom_1 : OneHom A B).toFun (star a) = star ((↑toMonoidHom_1 : OneHom A B).toFun a))
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
          { toMonoidHom := toMonoidHom, map_star' := map_star' })
        ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
          { toMonoidHom := toMonoidHom_1, map_star' := map_star'_1 })),
    { toMonoidHom := toMonoidHom, map_star' := map_star' : A →⋆* B } =
      { toMonoidHom := toMonoidHom_1, map_star' := map_star'_1 }
⊢ { toMonoidHom := toMonoidHom, map_star' := map_star' : A →⋆* B } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
toMonoidHom : A →* B
map_star' : ∀ (a : A), (↑toMonoidHom : OneHom A B).toFun (star a) = star ((↑toMonoidHom : OneHom A B).toFun a)
toMonoidHom_1 : A →* B
map_star'_1 : ∀ (a : A), (↑toMonoidHom_1 : OneHom A B).toFun (star a) = star ((↑toMonoidHom_1 : OneHom A B).toFun a)
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) { toMonoidHom := toMonoidHom, map_star' := map_star' })
    ((fun (f : A →⋆* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
      { toMonoidHom := toMonoidHom_1, map_star' := map_star'_1 })
⊢ { toMonoidHom := toMonoidHom, map_star' := map_star' : A →⋆* B } =
    { toMonoidHom := toMonoidHom_1, map_star' := map_star'_1 }

Tactic:
simp_all
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f : A →⋆* B
⊢ Eq (α := (a : A) → B) (⇑f.toMonoidHom : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f g : A →⋆* 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.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f : A →⋆* 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.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f : A →⋆* 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.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f : A →* B
h : ∀ (a : A), (↑f : OneHom A B).toFun (star a) = star ((↑f : OneHom A B).toFun a)
⊢ Eq (α := (a : A) → B) (⇑{ toMonoidHom := f, map_star' := h : A →⋆* B } : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
inst : Monoid A
inst_1 : Star A
⊢ Eq (α := (a : A) → A) (⇑(StarMonoidHom.id A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
inst_4 : Monoid C
inst_5 : Star C
inst_6 : Monoid D
inst_7 : Star D
f : B →⋆* C
g : A →⋆* B
a : A
⊢ (↑(f.comp g.toMonoidHom) : OneHom A C).toFun (star a) = star ((↑(f.comp g.toMonoidHom) : OneHom A C).toFun a)

Tactic:
simp [map_star]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
inst_4 : Monoid C
inst_5 : Star C
f : B →⋆* C
g : A →⋆* 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.MonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
inst_4 : Monoid C
inst_5 : Star C
f : B →⋆* C
g : A →⋆* 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.MonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
inst_4 : Monoid C
inst_5 : Star C
inst_6 : Monoid D
inst_7 : Star D
f : C →⋆* D
g : B →⋆* C
h : A →⋆* B
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: StarMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f : A →⋆* B
⊢ comp (StarMonoidHom.id B) f = f

Tactic:
ext fun _ => rfl

Premises used: StarMonoidHom.ext, rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Star A
inst_2 : Monoid B
inst_3 : Star B
f : A →⋆* B
⊢ f.comp (StarMonoidHom.id A) = f

Tactic:
ext fun _ => rfl

Premises used: StarMonoidHom.ext, rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
inst : Monoid A
inst_1 : Star A
⊢ Eq.{u_2 + 1} (α := (a : A) → A) (⇑1 : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
inst : Monoid A
inst_1 : Star A
a : A
⊢ (1 : (a : A) → A) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Mul D
inst_4 : Star A
inst_5 : Star B
inst_6 : Star C
inst_7 : Star D
f g : A ≃⋆* B
h : f.toFun = g.toFun
mk :
  ∀ (toMulEquiv : A ≃* B) (map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a))
    (h : { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.toFun = g.toFun),
    { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.invFun = g.invFun →
      { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B } = g
⊢ f.invFun = g.invFun → f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Mul D
inst_4 : Star A
inst_5 : Star B
inst_6 : Star C
inst_7 : Star D
g : A ≃⋆* B
toMulEquiv : A ≃* B
map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a)
h : { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.toFun = g.toFun
mk :
  ∀ (toMulEquiv_1 : A ≃* B) (map_star'_1 : ∀ (a : A), toMulEquiv_1.toFun (star a) = star (toMulEquiv_1.toFun a))
    (h :
      { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.toFun =
        { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 : A ≃⋆* B }.toFun),
    { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.invFun =
        { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 : A ≃⋆* B }.invFun →
      { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B } =
        { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 }
⊢ { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.invFun = g.invFun →
    { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Mul D
inst_4 : Star A
inst_5 : Star B
inst_6 : Star C
inst_7 : Star D
toMulEquiv : A ≃* B
map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a)
toMulEquiv_1 : A ≃* B
map_star'_1 : ∀ (a : A), toMulEquiv_1.toFun (star a) = star (toMulEquiv_1.toFun a)
h :
  { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.toFun =
    { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 : A ≃⋆* B }.toFun
⊢ { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.invFun =
      { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 : A ≃⋆* B }.invFun →
    { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B } =
      { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 }

Tactic:
simp_all
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
f g : A ≃⋆* B
h : ∀ (a : A), Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
inst : Mul A
inst_1 : Star A
⊢ Eq (α := (a : A) → A) (⇑(StarMulEquiv.refl A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Mul D
inst_4 : Star A
inst_5 : Star B
inst_6 : Star C
inst_7 : Star D
e : A ≃⋆* B
b : B
⊢ e.symm.toFun (star b) = star (e.symm.toFun b)

Tactic:
simpa only [EquivLike.apply_inv_apply, EquivLike.inv_apply_apply] using
        congr_arg (EquivLike.inv e) (map_star e (EquivLike.inv e b)).symm

Premises used: StarHomClass.map_star, EquivLike.inv_apply_apply, congr_arg, EquivLike.inv, Eq.symm, EquivLike.apply_inv_apply
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
e : A ≃⋆* B
⊢ EquivLike.inv e = (⇑e.symm : (a : B) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
e : A ≃⋆* B
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, StarMulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
⊢ Function.Bijective (α := A ≃⋆* B) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, StarMulEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
e : A ≃* B
h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)
⊢ Eq (α := (a : A) → B) (⇑{ toMulEquiv := e, map_star' := h₁ : A ≃⋆* B } : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
f : A ≃⋆* B
⊢ Eq (α := (a : A) → B) (⇑f.toMulEquiv : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
f : A ≃⋆* B
⊢ f.symm.toMulEquiv = f.symm

Tactic:
rfl

Premises used: MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
inst : Mul A
inst_1 : Star A
⊢ Eq (α := A ≃⋆* A) (symm (StarMulEquiv.refl A)) (StarMulEquiv.refl A)

Tactic:
rfl

Premises used: MulEquiv.refl, StarMulEquiv.refl, Equiv.symm, MulEquiv.symm, Equiv.refl, StarMulEquiv.symm, rfl