awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * r • y)

Tactic:
case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 : A
r : R
x : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x)

Tactic:
smul_mem _ _ hpx

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 : A
r : R
x : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x)

Tactic:
exact smul_mem _ _ hpx

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) x
a : ∀ (x : A) (hx : x ∈ s), Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
a₁ :
  ∀ (x y : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
        ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
          (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
          Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x + y)
a₂ : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) 0
a₃ :
  ∀ (x y : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
        ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
          (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
          Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
a₄ :
  ∀ (r : R) (x : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x),
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x

Tactic:
induction hx using adjoin_induction with
    | mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | add x y _ _ hpx hpy => exact add_mem hpx hpy
    | zero => exact zero_mem _
    | mul x y _ _ hpx hpy =>
      apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
      case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | smul r x _ hpx => exact smul_mem _ _ hpx

Premises used: Submodule.smul, Subsemigroup.subset_closure, Submodule.zero, ZeroMemClass.zero_mem, Submodule.subset_span, Submodule.add, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
apply : (↑(Subsemigroup.closure s) : Set A) ⊆ (↑(NonUnitalSubalgebra.toSubmodule (adjoin R s)) : Set A)
⊢ LE.le (α := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (NonUnitalSubalgebra.toSubmodule (adjoin R s))

Tactic:
apply span_le.2 _

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
⊢ LE.le (α := Subsemigroup A) (Subsemigroup.closure s)
    (NonUnitalSubsemiring.toSubsemigroup (NonUnitalSubalgebra.toNonUnitalSubsemiring (adjoin R s)))

Tactic:
Subsemigroup.closure_le.2 (subset_adjoin R)

Premises used: Iff.mpr, NonUnitalAlgebra.subset_adjoin, Subsemigroup.closure_le
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
⊢ LE.le (α := Subsemigroup A) (Subsemigroup.closure s)
    (NonUnitalSubsemiring.toSubsemigroup (NonUnitalSubalgebra.toNonUnitalSubsemiring (adjoin R s)))

Tactic:
exact Subsemigroup.closure_le.2 (subset_adjoin R)

Premises used: Iff.mpr, Subsemigroup.closure_le
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
gc : GaloisConnection (β := NonUnitalSubalgebra R A) (adjoin R) SetLike.coe
u : NonUnitalSubalgebra R A → Set A
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (adjoin R ⊥) ⊥

Tactic:
apply GaloisConnection.l_bot

Premises used: GaloisConnection.l_bot
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ GaloisConnection (β := NonUnitalSubalgebra R A) (adjoin R) SetLike.coe

Tactic:
NonUnitalAlgebra.gc

Premises used: NonUnitalAlgebra.gc
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (adjoin R Set.univ) ⊤

Tactic:
eq_top_iff.2 fun _x hx => subset_adjoin R hx

Premises used: Iff.mpr, eq_top_iff, NonUnitalAlgebra.subset_adjoin
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : IsScalarTower R B B
inst_10 : SMulCommClass R B B
f : F
s : Set A
⊢ Eq (α := NonUnitalSubalgebra R B) (map f (adjoin R s)) (adjoin R ((⇑f : (a : A) → B) '' s))

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) NonUnitalAlgebra.gi.gc
    NonUnitalAlgebra.gi.gc fun _t => rfl

Premises used: GaloisConnection.l_comm_of_u_comm, Set.image_preimage, NonUnitalSubalgebra.gc_map_comap, rfl, NonUnitalAlgebra.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : IsScalarTower R B B
inst_10 : SMulCommClass R B B
f : F
x : A
⊢ Eq (α := NonUnitalSubalgebra R B) (map f (adjoin R {x})) (adjoin R (singleton (α := B) ((f : (a : A) → B) x : B)))

Tactic:
simp [NonUnitalAlgHom.map_adjoin]

Premises used: NonUnitalAlgHom.map_adjoin
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ (↑⊤ : Set A) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq.{v + 1} (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq.{v + 1} (α := NonUnitalSubsemiring A) (NonUnitalSubalgebra.toNonUnitalSubsemiring.{u, v} (R := R) ⊤) ⊤

Tactic:
rfl

Premises used: NonUnitalSubsemiring.copy, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq.{u_3 + 1} (α := NonUnitalSubring A) (NonUnitalSubalgebra.toNonUnitalSubring.{u_2, u_3} (R := R) ⊤) ⊤

Tactic:
rfl

Premises used: NonUnitalSubsemiring.copy, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ S.toSubmodule = ⊤ ↔ S = ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : NonUnitalSubalgebra R A
⊢ Eq.{u_3 + 1} (α := NonUnitalSubring A) S.toNonUnitalSubring ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra 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: NonUnitalAlgebra.mem_sup_left, NonUnitalAlgebra.mem_sup_right, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : IsScalarTower R B B
inst_10 : SMulCommClass R B B
f : F
S T : NonUnitalSubalgebra R A
⊢ Eq (α := NonUnitalSubalgebra R B) (NonUnitalSubalgebra.map f (S ⊔ T))
    (NonUnitalSubalgebra.map f S ⊔ NonUnitalSubalgebra.map f T)

Tactic:
(NonUnitalSubalgebra.gc_map_comap f).l_sup

Premises used: NonUnitalSubalgebra.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : IsScalarTower R B B
inst_10 : SMulCommClass R B B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S T : NonUnitalSubalgebra R A
⊢ Eq (α := NonUnitalSubalgebra R B) (NonUnitalSubalgebra.map f (S ⊓ T))
    (NonUnitalSubalgebra.map f S ⊓ NonUnitalSubalgebra.map f T)

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ (↑(S ⊓ T) : Set A) = (↑S : Set A) ∩ (↑T : Set A)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra 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.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ (S ⊓ T).toSubmodule = S.toSubmodule ⊓ T.toSubmodule

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ (S ⊓ T).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring ⊓ T.toNonUnitalSubsemiring

Tactic:
rfl

Premises used: NonUnitalSubsemiring.copy, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ (↑(sInf S) : Set A) = ⋂ s ∈ S, (↑s : Set A)

Tactic:
sInf_image

Premises used: Set.iInter, setOf, sInf_image
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

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

Premises used: Set.mem_iInter₂, SetLike.mem_coe, NonUnitalAlgebra.coe_sInf
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ (↑(sInf S).toSubmodule : Set A) = (↑(sInf (NonUnitalSubalgebra.toSubmodule '' S)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ (↑(sInf S).toNonUnitalSubsemiring : Set A) = (↑(sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ (↑(⨅ (i : ι), S i) : Set A) = ⋂ (i : ι), (↑(S i) : Set A)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra 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, NonUnitalAlgebra.mem_sInf
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
ι : Sort u_2
inst_9 : Nonempty ι
inst_10 : IsScalarTower R B B
inst_11 : SMulCommClass R B B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : ι → NonUnitalSubalgebra R A
a : (↑(NonUnitalSubalgebra.map f (⨅ (i : ι), S i)) : Set B) = (↑(⨅ (i : ι), NonUnitalSubalgebra.map f (S i)) : Set B)
⊢ Eq (α := NonUnitalSubalgebra R B) (NonUnitalSubalgebra.map f (⨅ (i : ι), S i))
    (⨅ (i : ι), NonUnitalSubalgebra.map f (S i))

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
ι : Sort u_2
inst_9 : Nonempty ι
inst_10 : IsScalarTower R B B
inst_11 : SMulCommClass R B B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : ι → NonUnitalSubalgebra R A
⊢ (↑(NonUnitalSubalgebra.map f (⨅ (i : ι), S i)) : Set B) = (↑(⨅ (i : ι), NonUnitalSubalgebra.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
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ (↑(NonUnitalSubalgebra.toSubmodule (⨅ (i : ι), S i)) : Set A) = (↑(⨅ (i : ι), (S i).toSubmodule) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
rw : Membership.mem (γ := Submodule R A) (Submodule.span R (↑⊥ : Set A)) x ↔ x = 0
rw₁ : Membership.mem (γ := Submodule R A) (R ∙ 0) x ↔ x = 0
rw₂ : Membership.mem (γ := Submodule R A) ⊥ x ↔ x = 0
rw₃ rw₄ : x = 0 ↔ x = 0
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure ∅) : Set A)) x ↔ x = 0

Tactic:
rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot,
      Submodule.span_zero_singleton, Submodule.mem_bot]

Premises used: NonUnitalSubsemiring.closure_empty, Submodule.mem_bot, NonUnitalSubsemiring.coe_bot, Submodule.span_zero_singleton
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
h :
  ∀ (x : A),
    Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule ⊥) x ↔ Membership.mem (γ := Submodule R A) ⊥ x
⊢ Eq.{v + 1} (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule ⊥) ⊥

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
⊢ Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule ⊥) x ↔ Membership.mem (γ := Submodule R A) ⊥ x

Tactic:
simp only [mem_bot, NonUnitalSubalgebra.mem_toSubmodule, Submodule.mem_bot]

Premises used: Submodule.mem_bot, NonUnitalSubalgebra.mem_toSubmodule, NonUnitalAlgebra.mem_bot
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ (↑⊥ : Set A) = {0}

Tactic:
simp [Set.ext_iff, NonUnitalAlgebra.mem_bot]

Premises used: Set.ext_iff, NonUnitalAlgebra.mem_bot
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
rw : Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x
⊢ x ∈ S

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x

Tactic:
mem_top

Premises used: NonUnitalAlgebra.mem_top
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x

Tactic:
exact mem_top

Premises used: NonUnitalAlgebra.mem_top