awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x
h : p a x ha hx
⊢ p a (star x) ha ⋯

Tactic:
star_right _ _ _ _ h
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x
h : p a x ha hx
⊢ p a (star x) ha ⋯

Tactic:
exact star_right _ _ _ _ h
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
⊢ LE.le (α := Subalgebra R A) (Algebra.adjoin R (s ∪ star s))
    (Subalgebra.centralizer R (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A))

Tactic:
Algebra.adjoin_le_centralizer_centralizer R (s ∪ star s)

Premises used: Algebra.adjoin_le_centralizer_centralizer, Union.union, Star.star
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
h :
  (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) = (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A)
⊢ LE.le (α := Subalgebra R A) (Algebra.adjoin R (s ∪ star s))
    (Subalgebra.centralizer R ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)))

Tactic:
convert! Algebra.adjoin_le_centralizer_centralizer R (s ∪ star s)

Premises used: Algebra.adjoin_le_centralizer_centralizer, Union.union, Star.star
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
h : (↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A) = (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A)
⊢ (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) = (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A)

Tactic:
rw [StarMemClass.star_coe_eq]

Premises used: StarMemClass.star_coe_eq
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
⊢ (↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A) = (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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
⊢ LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))

Tactic:
have := adjoin_le_centralizer_centralizer R s
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
⊢ IsMulCommutative.{u_3} ↥(adjoin R s)

Tactic:
.of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_

Premises used: IsMulCommutative.of_setLike_mul_comm
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
refine :
  ∀ (x : A) (h₁ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x) (x_1 : A)
    (h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1), x * x_1 = x_1 * x
⊢ IsMulCommutative.{u_3} ↥(adjoin R s)

Tactic:
refine .of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1
⊢ ∀ 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
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
⊢ Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x

Tactic:
apply this at h₁
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
⊢ Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1

Tactic:
apply this at h₂
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra 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 (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
⊢ x ∈ (s ∪ star s).centralizer.centralizer

Tactic:
rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂

Premises used: SetLike.mem_coe, StarSubalgebra.coe_centralizer_centralizer
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra 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 (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
h₃ : x ∈ (s ∪ star s).centralizer.centralizer
⊢ x_1 ∈ (s ∪ star s).centralizer.centralizer

Tactic:
rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂

Premises used: SetLike.mem_coe, StarSubalgebra.coe_centralizer_centralizer
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra 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₁ : x ∈ (s ∪ star s).centralizer.centralizer
h₂ : x_1 ∈ (s ∪ star s).centralizer.centralizer
⊢ x * x_1 = x_1 * x

Tactic:
Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂

Premises used: Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : 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 (α := StarSubalgebra 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₁ : x ∈ (s ∪ star s).centralizer.centralizer
h₂ : x_1 ∈ (s ∪ star s).centralizer.centralizer
⊢ x * x_1 = x_1 * x

Tactic:
exact Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂

Premises used: Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
S : Type u_5
inst_10 : SetLike S A
inst_11 : MulMemClass S A
inst_12 : StarMemClass S A
s : S
inst_13 : IsMulCommutative.{u_3} ↥s
⊢ IsMulCommutative.{u_3} ↥(adjoin R (↑s : Set A))

Tactic:
isMulCommutative_adjoin R
    (fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂)
    (fun _ h₁ _ h₂ => setLike_mul_comm h₁ (star_mem h₂))

Premises used: StarAlgebra.isMulCommutative_adjoin, setLike_mul_comm, StarMemClass.star_mem
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
x : A
inst_10 : IsStarNormal x
⊢ ∀ (x_1 : A), Membership.mem (γ := Set A) {x} x_1 → ∀ (y : A), Membership.mem (γ := Set A) {x} y → x_1 * y = y * x_1

Tactic:
grind
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
x : A
inst_10 : IsStarNormal x
⊢ ∀ (a : A), Membership.mem (γ := Set A) {x} a → ∀ (b : A), Membership.mem (γ := Set A) {x} b → a * star b = star b * a

Tactic:
grind
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
⊢ (↑⊤ : Set A) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
h : ∀ (x : A), Membership.mem (γ := Subalgebra R A) (toSubalgebra ⊤) x ↔ Membership.mem (γ := Subalgebra R A) ⊤ x
⊢ Eq.{u_3 + 1} (α := Subalgebra R A) (toSubalgebra ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
x : A
⊢ Membership.mem (γ := Subalgebra R A) (toSubalgebra ⊤) x ↔ Membership.mem (γ := Subalgebra R A) ⊤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ S.toSubalgebra = ⊤ ↔ S = ⊤

Tactic:
StarSubalgebra.toSubalgebra_injective.eq_iff' top_toSubalgebra

Premises used: Function.Injective.eq_iff', StarSubalgebra.toSubalgebra_injective, StarSubalgebra.top_toSubalgebra
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S T : StarSubalgebra R A
x : A
⊢ x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left; (this ·)

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S T : StarSubalgebra R A
x : A
⊢ x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right; (this ·)

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S T : StarSubalgebra R A
x y : A
hx : x ∈ S
hy : y ∈ T
⊢ x * y ∈ S ⊔ T

Tactic:
mul_mem (mem_sup_left hx) (mem_sup_right hy)

Premises used: StarSubalgebra.mem_sup_left, StarSubalgebra.mem_sup_right, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
f : A →⋆ₐ[R] B
S T : StarSubalgebra R A
⊢ Eq (α := StarSubalgebra R B) (map f (S ⊔ T)) (map f S ⊔ map f T)

Tactic:
(StarSubalgebra.gc_map_comap f).l_sup

Premises used: StarSubalgebra.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
f : A →⋆ₐ[R] B
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S T : StarSubalgebra R A
⊢ Eq (α := StarSubalgebra R B) (map f (S ⊓ T)) (map f S ⊓ map f T)

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S T : StarSubalgebra R A
⊢ (↑(S ⊓ T) : Set A) = (↑S : Set A) ∩ (↑T : Set A)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S T : StarSubalgebra R A
x : A
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S T : StarSubalgebra R A
h : ∀ (x : A), x ∈ (S ⊓ T).toSubalgebra ↔ x ∈ S.toSubalgebra ⊓ T.toSubalgebra
⊢ (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S T : StarSubalgebra R A
x : A
⊢ x ∈ (S ⊓ T).toSubalgebra ↔ x ∈ S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : Set (StarSubalgebra R A)
⊢ (↑(sInf S) : Set A) = ⋂ s ∈ S, (↑s : Set A)

Tactic:
sInf_image

Premises used: Set.iInter, setOf, sInf_image
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : Set (StarSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Premises used: StarSubalgebra.coe_sInf, Set.mem_iInter₂, SetLike.mem_coe
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : Set (StarSubalgebra R A)
⊢ (↑(sInf S).toSubalgebra : Set A) = (↑(sInf (toSubalgebra '' S)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ (↑(⨅ (i : ι), S i) : Set A) = ⋂ (i : ι), (↑(S i) : Set A)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, StarSubalgebra.mem_sInf
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
ι : Sort u_5
inst_10 : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
s : ι → StarSubalgebra R A
a : (↑(map f (iInf s)) : Set B) = (↑(⨅ (i : ι), map f (s i)) : Set B)
⊢ Eq (α := StarSubalgebra R B) (map f (iInf s)) (⨅ (i : ι), map f (s i))

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
ι : Sort u_5
inst_10 : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
s : ι → StarSubalgebra R A
⊢ (↑(map f (iInf s)) : Set B) = (↑(⨅ (i : ι), map f (s i)) : Set B)

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, Set.injOn_of_injective