awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : (↑x : A) ∈ T
⊢ Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf T hT : (a : ↥T) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ T) (↑x : A) hx) : B)
    ((f i : (a : ↥(K i)) → B) x : B)
have subst : ∀ (hx : (↑x : A) ∈ iSup K),
  Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf (iSup K) sorry : (a : ↥(iSup K)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)
Tactic: subst hT
Cleared hypotheses: T, hT, hx
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : (↑x : A) ∈ iSup K
⊢ Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)
have dsimp : Eq.{w + 1} (α := B)
  (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
      (↑(iSup K) : Set A) sorry (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
    B)
  ((f i : (a : ↥(K i)) → B) x : B)
Tactic: dsimp [iSupLift]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : (↑x : A) ∈ K i
⊢ Eq.{w + 1} (α := B) ((iSupLift K dir f hf T hT : (a : ↥T) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
have subst : ∀ (x : ↥(iSup K)) (hx : (↑x : A) ∈ K i),
  Eq.{w + 1} (α := B) ((iSupLift K dir f hf (iSup K) sorry : (a : ↥(iSup K)) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
Tactic: subst hT
Cleared hypotheses: T, hT, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : (↑x : A) ∈ K i
⊢ Eq.{w + 1} (α := B) ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
have dsimp : Eq.{w + 1} (α := B)
  (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
      (↑(iSup K) : Set A) sorry x :
    B)
  ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
Tactic: dsimp [iSupLift]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
have simp : (∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ (x : A) (x_1 : x ∈ s), star x * z = z * star x)
Tactic: simp only [Set.mem_union, or_imp, forall_and, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
⊢ (↑(centralizer R Set.univ) : Set A) = (↑(center R A) : Set A)
have rw : Set.centralizer (Set.univ ∪ star Set.univ) = (↑(center R A) : Set A)
Tactic: rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
rw : Set.centralizer (Set.univ ∪ star Set.univ) = (↑(center R A) : Set A)
⊢ (↑(centralizer R Set.univ) : Set A) = (↑(center R A) : Set A)
have rw₁ : Set.centralizer Set.univ = (↑(center R A) : Set A)
Tactic: rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
rw : Set.centralizer (Set.univ ∪ star Set.univ) = (↑(center R A) : Set A)
rw₁ : Set.centralizer Set.univ = (↑(center R A) : Set A)
⊢ (↑(centralizer R Set.univ) : Set A) = (↑(center R A) : Set A)
have rw₂ : Set.centralizer Set.univ = Set.center A
Tactic: rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
rw : Set.centralizer (Set.univ ∪ star Set.univ) = (↑(center R A) : Set A)
rw₁ : Set.centralizer Set.univ = (↑(center R A) : Set A)
rw₂ : Set.centralizer Set.univ = Set.center A
⊢ (↑(centralizer R Set.univ) : Set A) = (↑(center R A) : Set A)
have rw₃ : Set.center A = Set.center A
Tactic: rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw : ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
rw :
  ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw₁ : ((↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
rw :
  ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₁ : ((↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw₂ : (↑(centralizer R s) : Set A).centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
rw :
  ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₁ : ((↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₂ : (↑(centralizer R s) : Set A).centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw₃ : (s ∪ star s).centralizer.centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ LE.le (α := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s))
    (NonUnitalSubalgebra.centralizer R ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)))
have h : (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) =
  (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A)
Tactic: convert! NonUnitalAlgebra.adjoin_le_centralizer_centralizer R (s ∪ star s)
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) =
    (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A)
have h : (↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A) =
  (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A)
Tactic: rw [StarMemClass.star_coe_eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
⊢ IsMulCommutative.{v} ↥(adjoin R s)
have this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
Tactic: have := adjoin_le_centralizer_centralizer R s
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
⊢ IsMulCommutative.{v} ↥(adjoin R s)
have refine : ∀ (x : A) (h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x) (x_1 : A)
  (h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1), x * x_1 = x_1 * x
Tactic: refine .of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1
⊢ x * x_1 = x_1 * x
have hcomm₁ : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
Tactic: have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
    Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha)
      (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
⊢ x * x_1 = x_1 * x
have h₃ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
Tactic: apply this at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
⊢ x * x_1 = x_1 * x
have h₃ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
Tactic: apply this at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
⊢ x * x_1 = x_1 * x
have h₃ : x ∈ (s ∪ star s).centralizer.centralizer
Tactic: rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
h₃ : x ∈ (s ∪ star s).centralizer.centralizer
⊢ x * x_1 = x_1 * x
have h₄ : x_1 ∈ (s ∪ star s).centralizer.centralizer
Tactic: rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubsemiring (goal)
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
p q : NonUnitalStarSubsemiring R
h :
  Eq.{v + 1} (α := Set R) ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := p))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := q))
⊢ p = q
have mk : ∀ (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
  (star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier)
  (h :
    Eq.{v + 1} (α := Set R)
      ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
        { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
      ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := q))),
  { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubsemiring (goal)
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
q : NonUnitalStarSubsemiring R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier
h :
  Eq.{v + 1} (α := Set R)
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := q))
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } = q
have mk : ∀ (toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R)
  (star_mem'_1 : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring_1.carrier), star a ∈ toNonUnitalSubsemiring_1.carrier)
  (h :
    Eq.{v + 1} (α := Set R)
      ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
        { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
      ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
        { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }))),
  { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubsemiring (goal)
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier
toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R
star_mem'_1 : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring_1.carrier), star a ∈ toNonUnitalSubsemiring_1.carrier
h :
  Eq.{v + 1} (α := Set R)
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }))
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }
have mk : toNonUnitalSubsemiring = toNonUnitalSubsemiring_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubsemiring (goal)
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
x : R
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.NonUnitalSubsemiring (goal)
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
x : R
hx : x ∈ s
⊢ star x ∈ s
have rw : ∀ (hx : x ∈ (↑S : Set R)), star x ∈ (↑S : Set R)
Tactic: rw [hs] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Star.Pi (goal)
Goal:
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst : Star α
⊢ star (Sum.elim x y) = Sum.elim (star x) (star y)
have h : ∀ (x_1 : I ⊕ J), star (Sum.elim x y) x_1 = Sum.elim (star x) (star y) x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Star.Pi (goal)
Goal:
I : Type u_1
J : Type u_2
α : Type u_3
x_1 : I → α
y : J → α
inst : Star α
x : I ⊕ J
⊢ star (Sum.elim x_1 y) x = Sum.elim (star x_1) (star y) x
have h : ∀ (val : I), star (Sum.elim x_1 y) (Sum.inl val) = Sum.elim (star x_1) (star y) (Sum.inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Star.Pi (goal)
Goal:
I : Type u_1
J : Type u_2
α : Type u_3
x_1 : I → α
y : J → α
inst : Star α
x : I ⊕ J
h : ∀ (val : I), star (Sum.elim x_1 y) (Sum.inl val) = Sum.elim (star x_1) (star y) (Sum.inl val)
⊢ star (Sum.elim x_1 y) x = Sum.elim (star x_1) (star y) x
have h₁ : ∀ (val : J), star (Sum.elim x_1 y) (Sum.inr val) = Sum.elim (star x_1) (star y) (Sum.inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
s : Set α
inst : InvolutiveStar α
⊢ star '' s = star ⁻¹' s
have h₁ : Function.LeftInverse.{u_1 + 1, u_1 + 1} (α := α) star star
Tactic: rw [image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
s : Set α
inst : InvolutiveStar α
h₁ : Function.LeftInverse.{u_1 + 1, u_1 + 1} (α := α) star star
⊢ star '' s = star ⁻¹' s
have h₂ : Function.RightInverse.{u_1 + 1, u_1 + 1} (α := α) star star
Tactic: rw [image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : InvolutiveStar α
s t : Set α
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆
have rw : s⋆⋆ ⊆ t⋆ ↔ s ⊆ t⋆
Tactic: rw [← star_subset_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : InvolutiveStar α
s t : Set α
rw : s⋆⋆ ⊆ t⋆ ↔ s ⊆ t⋆
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆
have rw₁ : s ⊆ t⋆ ↔ s ⊆ t⋆
Tactic: rw [← star_subset_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
β : Type u_2
inst : InvolutiveStar β
x : β
⊢ Eq (α := Set β) {x}⋆ {x⋆}
have h : ∀ (y : β), Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y
Tactic: ext1 y