awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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 _)
      (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
have 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
Tactic: erw [Submodule.coe_subtype, Submodule.coe_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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 _)
      (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)
have 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)
Tactic: erw [Submodule.coe_subtype, Submodule.coe_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Star.MonoidHom (goal)
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)
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Star.MonoidHom (goal)
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)
⊢ { toMonoidHom := toMonoidHom, map_star' := map_star' : A →⋆* B } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Star.MonoidHom (goal)
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
⊢ f.invFun = g.invFun → f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Star.MonoidHom (goal)
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
⊢ { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B }.invFun = g.invFun →
    { toMulEquiv := toMulEquiv, map_star' := map_star' : A ≃⋆* B } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Star.MonoidHom (goal)
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
e₂ : B ≃⋆* C
a : A
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))
have rw : e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
Tactic: rw [e₁.map_star', e₂.map_star']
-- Lean 4 proof step from Mathlib.Algebra.Star.MonoidHom (goal)
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
e₂ : B ≃⋆* C
a : A
rw : e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))
have rw₁ : star (e₂.toFun (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
Tactic: rw [e₁.map_star', e₂.map_star']
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
p q : NonUnitalStarSubalgebra R A
h :
  Eq.{v + 1} (α := Set A) ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := p))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := q))
⊢ p = q
have mk : ∀ (toNonUnitalSubalgebra : NonUnitalSubalgebra R A)
  (star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier)
  (h :
    Eq.{v + 1} (α := Set A)
      ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
        { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
      ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := q))),
  { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
q : NonUnitalStarSubalgebra R A
toNonUnitalSubalgebra : NonUnitalSubalgebra R A
star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier
h :
  Eq.{v + 1} (α := Set A)
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := q))
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } = q
have mk : ∀ (toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A)
  (star_mem'_1 : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra_1.carrier), star a ∈ toNonUnitalSubalgebra_1.carrier)
  (h :
    Eq.{v + 1} (α := Set A)
      ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
        { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
      ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
        { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }))),
  { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
toNonUnitalSubalgebra : NonUnitalSubalgebra R A
star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier
toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A
star_mem'_1 : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra_1.carrier), star a ∈ toNonUnitalSubalgebra_1.carrier
h :
  Eq.{v + 1} (α := Set A)
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }))
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }
have mk : toNonUnitalSubalgebra = toNonUnitalSubalgebra_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubalgebra = T.toNonUnitalSubalgebra
x : A
⊢ x ∈ S ↔ x ∈ T
have rw : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ T
Tactic: rw [← mem_toNonUnitalSubalgebra, ← mem_toNonUnitalSubalgebra, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubalgebra = T.toNonUnitalSubalgebra
x : A
rw : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ T
⊢ x ∈ S ↔ x ∈ T
have rw₁ : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ T.toNonUnitalSubalgebra
Tactic: rw [← mem_toNonUnitalSubalgebra, ← mem_toNonUnitalSubalgebra, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubalgebra = T.toNonUnitalSubalgebra
x : A
rw : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ T
rw₁ : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ T.toNonUnitalSubalgebra
⊢ x ∈ S ↔ x ∈ T
have rw₂ : x ∈ T.toNonUnitalSubalgebra ↔ x ∈ T.toNonUnitalSubalgebra
Tactic: rw [← mem_toNonUnitalSubalgebra, ← mem_toNonUnitalSubalgebra, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
x : A
hx : x ∈ s
⊢ star x ∈ (S.copy s hs).carrier
have change : star x ∈ s
Tactic: change star x ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
x : A
hx : x ∈ s
⊢ star x ∈ s
have rw : ∀ (hx : x ∈ (↑S : Set A)), star x ∈ (↑S : Set A)
Tactic: rw [hs] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T
have rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
Tactic: rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
⊢ x ∈ S ↔ x ∈ T
have rw₁ : x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
Tactic: rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
rw₁ : x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
⊢ x ∈ S ↔ x ∈ T
have rw₂ : x ∈ T.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
Tactic: rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
g : B → A
f : F
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : ↥(NonUnitalStarAlgHom.range f)
x' : A
hx' : (f : (a : A) → B) x' = (↑x : B)
⊢ (f : (a : A) → B) (g (↑x : B)) = (↑x : B)
have rw : Eq.{w + 1} (α := B) ((f : (a : A) → B) (g ((f : (a : A) → B) x')) : B) ((f : (a : A) → B) x' : B)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
g : B → A
f : F
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : ↥(NonUnitalStarAlgHom.range f)
x' : A
hx' : (f : (a : A) → B) x' = (↑x : B)
rw : Eq.{w + 1} (α := B) ((f : (a : A) → B) (g ((f : (a : A) → B) x')) : B) ((f : (a : A) → B) x' : B)
⊢ (f : (a : A) → B) (g (↑x : B)) = (↑x : B)
have rw₁ : Eq.{w + 1} (α := B) ((f : (a : A) → B) x' : B) ((f : (a : A) → B) x' : B)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
s : Set A
a : A
h :
  a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
⊢ star a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
have rwa : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s)) (star a)
Tactic: rwa [NonUnitalSubalgebra.mem_carrier, ← NonUnitalSubalgebra.mem_star_iff,
      NonUnitalSubalgebra.star_adjoin_comm, Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
s : Set A
a : A
h :
  a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s)) (star a)
⊢ star a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
have rwa₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (star (NonUnitalAlgebra.adjoin R (s ∪ star s))) a
Tactic: rwa [NonUnitalSubalgebra.mem_carrier, ← NonUnitalSubalgebra.mem_star_iff,
      NonUnitalSubalgebra.star_adjoin_comm, Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
s : Set A
a : A
h :
  a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s)) (star a)
rwa₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (star (NonUnitalAlgebra.adjoin R (s ∪ star s))) a
⊢ star a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
have rwa₂ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star (s ∪ star s))) a
Tactic: rwa [NonUnitalSubalgebra.mem_carrier, ← NonUnitalSubalgebra.mem_star_iff,
      NonUnitalSubalgebra.star_adjoin_comm, Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
s : Set A
a : A
h :
  a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s)) (star a)
rwa₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (star (NonUnitalAlgebra.adjoin R (s ∪ star s))) a
rwa₂ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star (s ∪ star s))) a
⊢ star a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
have rwa₃ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star s ∪ star (star s))) a
Tactic: rwa [NonUnitalSubalgebra.mem_carrier, ← NonUnitalSubalgebra.mem_star_iff,
      NonUnitalSubalgebra.star_adjoin_comm, Set.union_star, star_star, Set.union_comm]