mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
⊢ ⨆ i, Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑((x • s) • t) = ↑(x • s • t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑x = ↑y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.equivOfEq S ⋯ = AlgEquiv.refl

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
this : (⇑e ∘ fun i ↦ Submodule.comap p.subtype (A ↑i)) = fun i ↦ ⟨A ↑i, ⋯⟩
⊢ iSupIndep fun i ↦ Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
⊢ (f.comp S.val).range = map f S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (algebraMap (↥S) A).rangeS = S.toSubsemiring

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (algebraMap (↥S) A).range = S.toSubring

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
⊢ IsInternal fun i ↦ Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ T U : Subalgebra R A
h : S✝ ≤ T
α : Type u_1
β : Type u_2
inst✝ : IsDomain A
S : Subalgebra R A
r : ↥S
hr : IsRegular r
⊢ IsRegular ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ T U : Subalgebra R A
h : S✝ ≤ T
α : Type u_1
β : Type u_2
inst✝ : IsDomain A
S : Subalgebra R A
⊢ ∀ (r : ↥S) (m : A), ↑r • m = r • m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
N : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (N i)
inst✝² : (i : ι) → Module R (N i)
P : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (P i)
inst✝ : (i : ι) → Module R (P i)
u : (i : ι) → N i ≃+ P i
x : ⨁ (i : ι), N i
⊢ (map fun i ↦ (u i).symm.toAddMonoidHom) ((↑(map fun i ↦ (u i).toAddMonoidHom)).toFun x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (algebraMap R A) r ∈ Set.center A

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : x ∈ adjoin R s), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : x ∈ adjoin R s), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : x ∈ adjoin R s
hy : y ∈ adjoin R s
⊢ p x y hx hy

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ centralizer R s.centralizer.centralizer = centralizer R s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
N : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (N i)
inst✝² : (i : ι) → Module R (N i)
P : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (P i)
inst✝ : (i : ι) → Module R (P i)
u : (i : ι) → N i ≃+ P i
y : ⨁ (i : ι), P i
⊢ (↑(map fun i ↦ (u i).toAddMonoidHom)).toFun ((map fun i ↦ (u i).symm.toAddMonoidHom) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i : ℤ
⊢ (algebraMap ℤ R) 0 ∈ S.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) ↑i ∈ S.carrier
⊢ (algebraMap ℤ R) (↑i + 1) ∈ S.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
N : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (N i)
inst✝² : (i : ι) → Module R (N i)
P : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (P i)
inst✝ : (i : ι) → Module R (P i)
u : (i : ι) → N i ≃ₗ[R] P i
r : R
x : ⨁ (i : ι), N i
⊢ (congrAddEquiv fun i ↦ (u i).toAddEquiv).toFun (r • x) =
    (RingHom.id R) r • (congrAddEquiv fun i ↦ (u i).toAddEquiv).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ x * y ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
⊢ 1 ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ y ∈ span R ↑(Subsemigroup.closure s), 0 * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ x ∈ span R ↑(Subsemigroup.closure s), x * 0 ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
m : ι →₀ M
i : ι
⊢ ((finsuppLEquivDirectSum R M ι) m) i = m i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_1
inst✝² : DecidableEq ι
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ε : M →ₗ[R] N
m : ι →₀ M
⊢ (lmap fun x ↦ ε) ((finsuppLEquivDirectSum R M ι) m) = (finsuppLEquivDirectSum R N ι) (Finsupp.mapRange ⇑ε ⋯ m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ x + y ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
⊢ 0 ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x : R
⊢ (algebraMap R A) x ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toSubalgebra h1).toNonUnitalSubalgebra = S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
hx : x ∈ adjoin R s
hy : y ∈ adjoin R s
⊢ p x y hx hy

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * z ∈ span R ↑(Subsemigroup.closure s)
hyz : y * z ∈ span R ↑(Subsemigroup.closure s)
⊢ (x + y) * z ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * y ∈ span R ↑(Subsemigroup.closure s)
hyz : x * z ∈ span R ↑(Subsemigroup.closure s)
⊢ x * (y + z) ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ r • x * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ adjoin R (Subtype.val ⁻¹' s) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ r • x * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by simpa [smul_mul_assoc] using smul_mem _ _ hxy

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
⊢ R[↑n] = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ x * r • y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
s : Set A
⊢ adjoin R (insert ((algebraMap R A) x) s) = adjoin R s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ ↑(Subsemigroup.closure s) ⊆ ↑(adjoin R s).toSubmodule

Tactic:
change Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ (adjoin R s).toSubmodule = span R ↑(Subsemigroup.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : NonUnitalNonAssocSemiring A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
x : A
⊢ map f (adjoin R {x}) = adjoin R {f x}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ S.toSubmodule = ⊤ ↔ S = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
⊢ S.toNonUnitalSubring = ⊤ ↔ S = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(sInf S).toSubmodule = ↑(sInf (NonUnitalSubalgebra.toSubmodule '' S))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
this : ∃ z r, ∃ (_hr : r ∈ Submonoid.closure s), z • r = hd.prod
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(sInf S).toNonUnitalSubsemiring = ↑(sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by simp [iInf]

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : FunLike F A B
inst✝⁵ : NonUnitalAlgHomClass F R A B
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
ι : Sort u_2
inst✝² : Nonempty ι
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalSubalgebra R A
⊢ NonUnitalSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalSubalgebra.map f (S i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ i, S i).toSubmodule = ↑(⨅ i, (S i).toSubmodule)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ ⊥.toSubmodule = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ ↑⊥ = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
by

Goal state after: