awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rwa₃ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star s ∪ star (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 ∪ 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
rwa₃ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star s ∪ star (star s))) a
rwa₄ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star s ∪ 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 (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:
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
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
⊢ p a ha
have refine : ∀ (x : A) (hx : x ∈ s ∪ Star.star s), p x sorry
Tactic: refine NonUnitalAlgebra.adjoin_induction (fun x hx ↦ ?_) add zero mul smul 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
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx : x ∈ s ∪ Star.star s
⊢ p x ⋯
have hx₁ : x ∈ s ∨ Star.star x ∈ s
Tactic: push _ ∈ _ at hx
-- 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
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s ∨ Star.star x ∈ s
⊢ p x ⋯
have inl : ∀ (hx : x ∈ s), p x sorry
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- 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
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s ∨ Star.star x ∈ s
inl : ∀ (hx : x ∈ s), p x ⋯
⊢ p x ⋯
have inr : ∀ (hx : Star.star x ∈ s), p x sorry
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- 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
S : NonUnitalStarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ≤ (↑S : Set A)
have rw : s ∪ star s ⊆ (↑S : Set A) ↔ s ≤ (↑S : Set A)
Tactic: rw [← toNonUnitalSubalgebra_le_iff, adjoin_toNonUnitalSubalgebra,
    NonUnitalAlgebra.adjoin_le_iff, coe_toNonUnitalSubalgebra]
-- 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
⊢ Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (toNonUnitalSubalgebra (adjoin R s)))
    (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
have rw : Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (NonUnitalAlgebra.adjoin R (s ∪ star s)))
  (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
Tactic: rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]
-- 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
rw :
  Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (NonUnitalAlgebra.adjoin R (s ∪ star s)))
    (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
⊢ Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (toNonUnitalSubalgebra (adjoin R s)))
    (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
have rw₁ : Eq (α := Submodule R A) (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
  (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
Tactic: rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]
-- 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
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊤) ⊤
have h : ∀ (x : A),
  Membership.mem (γ := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊤) x ↔
    Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R : Type u
A : Type v
B : 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
ι : Sort u_1
inst_14 : Nonempty ι
inst_15 : IsScalarTower R B B
inst_16 : SMulCommClass R B B
inst_17 : StarModule R B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : ι → NonUnitalStarSubalgebra R A
⊢ Eq (α := NonUnitalStarSubalgebra R B) (map f (⨅ (i : ι), S i)) (⨅ (i : ι), map f (S i))
have a : (↑(map f (⨅ (i : ι), S i)) : Set B) = (↑(⨅ (i : ι), map f (S i)) : Set B)
Tactic: apply SetLike.coe_injective
-- 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
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ star ∅)) x ↔ x = 0
have rw : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ ∅)) x ↔ x = 0
Tactic: rw [Set.star_empty, Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot]
-- 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
x : A
rw : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ ∅)) x ↔ x = 0
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ star ∅)) x ↔ x = 0
have rw₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R ∅) x ↔ x = 0
Tactic: rw [Set.star_empty, Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot]
-- 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
x : A
rw : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ ∅)) x ↔ x = 0
rw₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R ∅) x ↔ x = 0
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ star ∅)) x ↔ x = 0
have rw₂ : Membership.mem (γ := NonUnitalSubalgebra R A) ⊥ x ↔ x = 0
Tactic: rw [Set.star_empty, Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot]
-- 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
x : A
rw : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ ∅)) x ↔ x = 0
rw₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R ∅) x ↔ x = 0
rw₂ : Membership.mem (γ := NonUnitalSubalgebra R A) ⊥ x ↔ x = 0
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ star ∅)) x ↔ x = 0
have rw₃ : x = 0 ↔ x = 0
Tactic: rw [Set.star_empty, Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot]
-- 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
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊥) ⊥
have h : ∀ (x : A),
  Membership.mem (γ := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊥) x ↔
    Membership.mem (γ := NonUnitalSubalgebra R A) ⊥ x
Tactic: ext x
-- 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 : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S
have rw : Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x
Tactic: rw [h]
-- 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 : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤
have h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x
Tactic: ext x
-- 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
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : IsScalarTower R B B
inst_12 : SMulCommClass R B B
inst_13 : StarModule R B
⊢ Eq (α := NonUnitalStarSubalgebra R (A × B)) (prod ⊤ ⊤) ⊤
have h : ∀ (x : A × B),
  Membership.mem (γ := NonUnitalStarSubalgebra R (A × B)) (prod ⊤ ⊤) x ↔
    Membership.mem (γ := NonUnitalStarSubalgebra R (A × B)) ⊤ x
Tactic: ext
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
inst_17 : 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
⊢ NonUnitalStarAlgHom.{u, v, w} R (↥T) B
have subst : NonUnitalStarAlgHom.{u, v, w} R (↥(iSup K)) B
Tactic: subst hT
Cleared hypotheses: T, hT
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
inst_17 : 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 j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
⊢ Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))
have let : ∀ (k : ι) (hik : K i ≤ K k) (hjk : K j ≤ K k),
  Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))
Tactic: let ⟨k, hik, hjk⟩ := dir i j
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
inst_17 : 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 j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
k : ι
hik : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
⊢ Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)
have rw : Eq.{w + 1} (α := B)
  (((f k).comp (inclusion hik) : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
  (((f k).comp (inclusion hjk) : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)
Tactic: rw [hf i k hik, hf j k hjk]
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
inst_17 : 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)
⊢ (↑(iSup K) : Set A) ⊆ ⋃ (i : ι), (↑(K i) : Set A)
have rw : Subset.{v} (α := Set A) (⋃ (i : ι), (↑(K i) : Set A)) (⋃ (i : ι), (↑(K i) : Set A))
Tactic: rw [coe_iSup_of_directed dir]