mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
y : R
hy : y ∈ I
z : R
hz : z ∈ J
⊢ y + z ∈ I ⊔ J

Tactic:
;

Goal state after:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
y : R
hy : y ∈ I
z : R
hz : z ∈ J
⊢ y + z ∈ I ⊔ J
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon }.ringCon ≤ I.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon }.ringCon ≤ I.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon }.ringCon ≤ J.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon }.ringCon ≤ J.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ J.ringCon
h2 : I.ringCon ≤ K.ringCon
⊢ I.ringCon ≤ { ringCon := J.ringCon ⊓ K.ringCon }.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ J.ringCon
h2 : I.ringCon ≤ K.ringCon
⊢ I.ringCon ≤ { ringCon := J.ringCon ⊓ K.ringCon }.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sSup (ringCon '' Set.range fun i ↦ I i) = sSup (Set.range fun i ↦ (I i).ringCon)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sSup (ringCon '' Set.range fun i ↦ I i) = sSup (Set.range fun i ↦ (I i).ringCon)
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (ringCon '' Set.range fun i ↦ I i) = Set.range fun i ↦ (I i).ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (ringCon '' Set.range fun i ↦ I i) = Set.range fun i ↦ (I i).ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i ↦ I i) ↔ x✝ ∈ Set.range fun i ↦ (I i).ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i ↦ I i) ↔ x✝ ∈ Set.range fun i ↦ (I i).ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sInf (ringCon '' Set.range fun i ↦ I i) = sInf (Set.range fun i ↦ (I i).ringCon)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sInf (ringCon '' Set.range fun i ↦ I i) = sInf (Set.range fun i ↦ (I i).ringCon)
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ x✝.ringCon ≤ ⊤.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ x✝.ringCon ≤ ⊤.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ ⊥.ringCon ≤ x✝.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ ⊥.ringCon ≤ x✝.ringCon
Module: Mathlib.Algebra.Algebra.Subalgebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ restrictScalars R V ↔ x ∈ V

Tactic:
mem_restrictScalars

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ V ↔ x ∈ V
Module: Mathlib.Algebra.Algebra.Subalgebra.Tower

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ Submodule.restrictScalars R 1 ↔ x✝ ∈ toSubmodule S

Tactic:
;

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ Submodule.restrictScalars R 1 ↔ x✝ ∈ toSubmodule S
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
T : Subalgebra R A :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
⊢ motive x

Tactic:
suffices iSup S ≤ T from this mem

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
T : Subalgebra R A :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
⊢ iSup S ≤ T
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Tactic:
;

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
;

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : A
⊢ r • ↑φ a ∈ (NonUnitalRingHom.srange ↑φ).carrier

Tactic:
;

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : A
⊢ r • ↑φ a ∈ (NonUnitalRingHom.srange ↑φ).carrier
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: case mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
q : Subalgebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h : (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ } = (fun s ↦ s.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
q : Subalgebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h : (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ } = (fun s ↦ s.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ } = q
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: case mk.mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
toSubsemiring✝¹ : Subsemiring A
algebraMap_mem'✝¹ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
toSubsemiring✝¹ : Subsemiring A
algebraMap_mem'✝¹ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: case mk.mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
toSubsemiring✝¹ : Subsemiring A
algebraMap_mem'✝¹ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝

Tactic:
;

Goal state after:
case mk.mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
toSubsemiring✝¹ : Subsemiring A
algebraMap_mem'✝¹ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
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 : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ * b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
;

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ * b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}
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 : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ + b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
;

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ + b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}
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
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
⊢ ∀ (r : R),
    (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
intro r

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
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
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
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
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ r • 1 ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ r • 1 ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
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✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ ↑((e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r)) =
    ↑((algebraMap R ↥(Subalgebra.map (↑e) S)) r)

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ ↑((e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r)) =
    ↑((algebraMap R ↥(Subalgebra.map (↑e) S)) r)
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
a✝ : ↥S
⊢ ↑((S.equivOfEq S ⋯) a✝) = ↑(AlgEquiv.refl a✝)

Tactic:
;

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
a✝ : ↥S
⊢ ↑((S.equivOfEq S ⋯) a✝) = ↑(AlgEquiv.refl a✝)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.toNonUnitalSubalgebra.toSubalgebra ⋯ =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }

Tactic:
;

Goal state after:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.toNonUnitalSubalgebra.toSubalgebra ⋯ =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }

Tactic:
;

Goal state after:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)

Tactic:
intro r

Goal state after:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
r : A
⊢ r ∈ Subalgebra.toSubmodule (adjoin R s) → r ∈ span R ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case gc
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
⊢ GaloisConnection (adjoin R) ?u

pp: case u
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
⊢ NonUnitalSubalgebra R A → Set A

Tactic:
;

Goal state after:
case gc
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
⊢ GaloisConnection (adjoin R) ?u

case u
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
⊢ NonUnitalSubalgebra R A → Set A
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 ∈ ⊤

Tactic:
;

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 : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
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
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
;

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 : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: 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✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
;

Goal state after:
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✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤