awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : S ≤ equalizer φ ψ
hT : T ≤ equalizer φ ψ
⊢ S ⊔ T ≤ equalizer φ ψ

Tactic:
sup_le hS hT

Premises used: sup_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : S ≤ equalizer φ ψ
hT : T ≤ equalizer φ ψ
⊢ S ⊔ T ≤ equalizer φ ψ

Tactic:
exact sup_le hS hT

Premises used: sup_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hST : Codisjoint S T
hS : Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑S : Set A)
hT : Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑T : Set A)
⊢ φ = ψ

Tactic:
DFunLike.ext _ _ fun _ ↦ eqOn_sup hS hT <| hST.eq_top.symm ▸ trivial

Premises used: trivial, DFunLike.ext, Eq.rec, AlgHom.eqOn_sup, Eq.symm, Codisjoint.eq_top
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R B
⊢ map f (comap f S) = S ⊓ f.range

Tactic:
SetLike.coe_injective Set.image_preimage_eq_inter_range

Premises used: SetLike.coe_injective, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R B
h : S ≤ f.range
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Premises used: inf_of_le_left, Subalgebra.map_comap_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : Subalgebra R B
⊢ S ≤ f.range

Tactic:
simp [(AlgHom.range_eq_top f).2 hf]

Premises used: Iff.mpr, AlgHom.range_eq_top
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b : S
this :
  ∀ (m : S) (hm : m ∈ M) (ha : m * a ∈ s),
    Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} b →
      Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a * b)
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} a →
    Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} b →
      Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a * b)

Tactic:
⟨m, hm, ha⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
this : ∀ (n : S) (hn : n ∈ M) (hb : n * b ∈ s), Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a * b)
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} b →
    Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a * b)

Tactic:
⟨n, hn, hb⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a * b)

Tactic:
⟨_, mul_mem hm hn, mul_mul_mul_comm m n a b ▸ mul_mem ha hb⟩

Premises used: mul_mul_mul_comm, Set.Mem, setOf, Eq.rec, And.intro, Exists.intro, Eq.symm, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a * b)

Tactic:
refine ⟨_, mul_mem hm hn, mul_mul_mul_comm m n a b ▸ mul_mem ha hb⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b : S
this :
  ∀ (m : S) (hm : m ∈ M) (ha : m * a ∈ s),
    Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} b →
      Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a + b)
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} a →
    Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} b →
      Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a + b)

Tactic:
⟨m, hm, ha⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
this : ∀ (n : S) (hn : n ∈ M) (hb : n * b ∈ s), Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a + b)
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} b →
    Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a + b)

Tactic:
⟨n, hn, hb⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a + b)

Tactic:
⟨_, mul_mem hn hm, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
refine : n * m * (a + b) ∈ s
⊢ Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a + b)

Tactic:
refine ⟨_, mul_mem hn hm, ?_⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
rw : n * (m * a) + m * (n * b) ∈ s
⊢ n * m * (a + b) ∈ s

Tactic:
rw [mul_add, mul_assoc, mul_comm n m, mul_assoc]

Premises used: mul_assoc, mul_comm, mul_add
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * (m * a) + m * (n * b) ∈ s

Tactic:
add_mem (mul_mem (H hn) ha) (mul_mem (H hm) hb)

Premises used: AddMemClass.add_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * (m * a) + m * (n * b) ∈ s

Tactic:
exact add_mem (mul_mem (H hn) ha) (mul_mem (H hm) hb)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s_1 : Subalgebra R S
M_1 : Submonoid S
H_1 : M_1 ≤ s_1.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
r : R
⊢ HMul.hMul (α := S) (β := S) (1 : S) ((algebraMap R S : (a : R) → S) r : S) ∈ s

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
x : S
⊢ x ∈ s.saturation M H ↔ ∃ m ∈ M, m • x ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
x : S
hx : x ∈ s
⊢ 1 * x ∈ s

Tactic:
simpa
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
⊢ (s.saturation M H).saturation M ⋯ = s.saturation M H

Tactic:
le_saturation.antisymm' fun x ⟨m, hm, n, hn, h⟩ ↦ ⟨_, M.mul_mem hn hm, mul_assoc n m x ▸ h⟩

Premises used: HMul.hMul, Submonoid.mul_mem, LE.le.antisymm', mul_assoc, Membership.mem, Eq.rec, _private.0.Subalgebra.saturation_saturation.match_1, And.intro, Exists.intro, Subalgebra.le_saturation, Eq.symm, Subalgebra.saturation
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
x y : S
hxy : x * y ∈ s.saturation M H
hx : x ∈ M
⊢ y ∈ s.saturation M H

Tactic:
saturation_saturation.le ⟨_, hx, hxy⟩

Premises used: Eq.le, Subalgebra.saturation_saturation, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
x y : S
hxy : x * y ∈ s.saturation M H
hy : y ∈ M
⊢ x ∈ s.saturation M H

Tactic:
mem_saturation_of_mul_mem_left (mul_comm x y ▸ hxy) hy

Premises used: Subalgebra.mem_saturation_of_mul_mem_left
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ s ⊆ (↑(adjoin R s) : Set A)

Tactic:
Algebra.gc.le_u_l s

Premises used: GaloisConnection.le_u_l, Algebra.gc
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
x : A
hx : x ∈ s
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R s) x

Tactic:
subset_adjoin hx

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
S : Subalgebra R A
H : s ⊆ (↑S : Set A)
⊢ adjoin R s ≤ S

Tactic:
Algebra.gc.l_le H

Premises used: GaloisConnection.l_le, Algebra.gc
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
a : A
H : a ∈ S
⊢ R[a] ≤ S

Tactic:
adjoin_le (Set.singleton_subset_iff.mpr H)

Premises used: Iff.mpr, Set.singleton_subset_iff, Algebra.adjoin_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R s) (sInf {p : Subalgebra R A | s ⊆ (↑p : Set A)})

Tactic:
le_antisymm (le_sInf fun _ h => adjoin_le h) (sInf_le subset_adjoin)

Premises used: Algebra.subset_adjoin, le_antisymm, sInf_le, Algebra.adjoin_le, le_sInf
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
S : Subalgebra R A
⊢ adjoin R s ≤ S ↔ s ⊆ (↑S : Set A)

Tactic:
Algebra.gc _ _

Premises used: Algebra.gc
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s t : Set A
H : s ⊆ t
⊢ LE.le (α := Subalgebra R A) (adjoin R s) (adjoin R t)

Tactic:
Algebra.gc.monotone_l H

Premises used: GaloisConnection.monotone_l, Algebra.gc
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
S : Subalgebra R A
h₁ : s ⊆ (↑S : Set A)
h₂ : S ≤ adjoin R s
⊢ adjoin R s = S

Tactic:
le_antisymm (adjoin_le h₁) h₂

Premises used: le_antisymm, Algebra.adjoin_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ adjoin R (↑S : Set A) = S

Tactic:
adjoin_eq_of_le _ (Set.Subset.refl _) subset_adjoin

Premises used: Set.Subset.refl, Algebra.subset_adjoin, Algebra.adjoin_eq_of_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
α : Type u_1
s : α → Set A
⊢ Eq (α := Subalgebra R A) (adjoin R (Set.iUnion s)) (⨆ (i : α), adjoin R (s i))

Tactic:
(@Algebra.gc R A _ _ _).l_iSup

Premises used: GaloisConnection.l_iSup, Set.iUnion, Algebra.gc
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq A
α : Type u_1
s : Finset α
f : ↥s → Finset A
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(s.attach.biUnion f) : Set A)) (⨆ (x : ↥s), adjoin R (↑(f x) : Set A))

Tactic:
simp [adjoin_iUnion]

Premises used: Algebra.adjoin_iUnion
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
p : (x : A) → Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
a b : A
w : Membership.mem (γ := Subalgebra R A) (adjoin R s) a
hpx : p a w
w_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) b
hpy : p b w_1
⊢ Membership.mem (γ := Set A) {x : A | ∃ (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x), p x hx} (a * b)

Tactic:
⟨_, mul _ _ _ _ hpx hpy⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
p : (x : A) → Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
a b : A
w : Membership.mem (γ := Subalgebra R A) (adjoin R s) a
hpx : p a w
w_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) b
hpy : p b w_1
⊢ Membership.mem (γ := Set A) {x : A | ∃ (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x), p x hx} (a * b)

Tactic:
exact ⟨_, mul _ _ _ _ hpx hpy⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
p : (x : A) → Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
a b : A
w : Membership.mem (γ := Subalgebra R A) (adjoin R s) a
hpx : p a w
w_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) b
hpy : p b w_1
⊢ Membership.mem (γ := Set A) {x : A | ∃ (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x), p x hx} (a + b)

Tactic:
⟨_, add _ _ _ _ hpx hpy⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
p : (x : A) → Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
a b : A
w : Membership.mem (γ := Subalgebra R A) (adjoin R s) a
hpx : p a w
w_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) b
hpy : p b w_1
⊢ Membership.mem (γ := Set A) {x : A | ∃ (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x), p x hx} (a + b)

Tactic:
exact ⟨_, add _ _ _ _ hpx hpy⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
x_1 : A
h : x_1 ∈ s
⊢ p x_1 z ⋯ ⋯

Tactic:
mem_mem _ _ h hz
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
x_1 : A
h : x_1 ∈ s
⊢ p x_1 z ⋯ ⋯

Tactic:
exact mem_mem _ _ h hz
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra 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 (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
r : R
⊢ p ((algebraMap R A : (a : R) → A) r) z ⋯ ⋯

Tactic:
algebraMap_left _ _ hz