awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)
have e_s : Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ⊆ ⋃₀ (SetLike.coe '' S)
Tactic: rw [Set.union_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
⊢ Membership.mem (α := A) (⋃₀ (SetLike.coe '' S)) ((algebraMap R A : (a : R) → A) x : A)
have e_s : ∀ (y : Subalgebra R A) (hy : y ∈ S),
  Membership.mem (α := A) (⋃₀ (SetLike.coe '' S)) ((algebraMap R A : (a : R) → A) x : A)
Tactic: obtain ⟨y, hy⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ Membership.mem (α := A) (⋃₀ (SetLike.coe '' S)) ((algebraMap R A : (a : R) → A) x : A)
have e_s : ∃ a ∈ S, Membership.mem (α := A) a ((algebraMap R A : (a : R) → A) x : A)
Tactic: simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
ι : Sort u_1
inst_5 : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
s : ι → Subalgebra R A
⊢ Subalgebra.map f (iInf s) = ⨅ (i : ι), Subalgebra.map f (s i)
have a : (↑(Subalgebra.map f (iInf s)) : Set B) = (↑(⨅ (i : ι), Subalgebra.map f (s i)) : Set B)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
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 : (a : R) → A) r)
T : Subalgebra R A :=
  { carrier := {x : A | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
⊢ motive x
have suffices : iSup S ≤ T
Tactic: suffices iSup S ≤ T from this mem
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
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 : (a : R) → A) r)
T : Subalgebra R A :=
  { carrier := {x : A | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
⊢ iSup S ≤ T
have rwa : ∀ (i : ι), S i ≤ T
Tactic: rwa [iSup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
⊢ motive x mem
have refine : ∃ (x_1 : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x), motive x x_1
Tactic: refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) ↦ hc
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S
have rw : Membership.mem (γ := Subalgebra R A) ⊤ x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤
have h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := Subalgebra R A) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
inst_5 : Subsingleton.{w + 1} (Subalgebra R B)
f g : A ≃ₐ[R] B
⊢ f = g
have rw : f.symm.symm = g
Tactic: rw [← f.symm_symm, Subsingleton.elim f.symm g.symm, g.symm_symm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
inst_5 : Subsingleton.{w + 1} (Subalgebra R B)
f g : A ≃ₐ[R] B
rw : f.symm.symm = g
⊢ f = g
have rw₁ : g.symm.symm = g
Tactic: rw [← f.symm_symm, Subsingleton.elim f.symm g.symm, g.symm_symm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
inst_5 : Subsingleton.{w + 1} (Subalgebra R B)
f g : A ≃ₐ[R] B
rw : f.symm.symm = g
rw₁ : g.symm.symm = g
⊢ f = g
have rw₂ : g = g
Tactic: rw [← f.symm_symm, Subsingleton.elim f.symm g.symm, g.symm_symm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 : Subalgebra R A
S : Subalgebra R R
⊢ S = default
have refine : S ≤ default
Tactic: refine le_antisymm ?_ bot_le
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
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 : 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)
⊢ Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑(S ⊔ T) : Set A)
have hS₁ : S ≤ equalizer φ ψ
Tactic: rw [← le_equalizer] at hS hT ⊢
Cleared hypotheses: hS, hT
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
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 : 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)
hS₁ : S ≤ equalizer φ ψ
⊢ Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑(S ⊔ T) : Set A)
have hT₁ : T ≤ equalizer φ ψ
Tactic: rw [← le_equalizer] at hS hT ⊢
Cleared hypotheses: hS, hT
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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
⊢ 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)
have 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)
Tactic: ⟨m, hm, ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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
⊢ 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)
have this : ∀ (n : S) (hn : n ∈ M) (hb : n * b ∈ s), Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a * b)
Tactic: ⟨n, hn, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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
⊢ 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)
have 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)
Tactic: ⟨m, hm, ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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
⊢ 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)
have this : ∀ (n : S) (hn : n ∈ M) (hb : n * b ∈ s), Membership.mem (γ := Set S) {x : S | ∃ m ∈ M, m * x ∈ s} (a + b)
Tactic: ⟨n, hn, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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)
have refine : n * m * (a + b) ∈ s
Tactic: refine ⟨_, mul_mem hn hm, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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 + b) ∈ s
have rw : n * (m * a) + m * (n * b) ∈ s
Tactic: rw [mul_add, mul_assoc, mul_comm n m, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
⊢ p x z hx ⋯
have mem : ∀ (x : A) (h : x ∈ s), p x z sorry sorry
Tactic: induction hx using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
mem : ∀ (x : A) (h : x ∈ s), p x z ⋯ ⋯
⊢ p x z hx ⋯
have mem₁ : ∀ (r : R), p ((algebraMap R A : (a : R) → A) r) z sorry sorry
Tactic: induction hx using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
mem : ∀ (x : A) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : ∀ (r : R), p ((algebraMap R A : (a : R) → A) r) z ⋯ ⋯
⊢ p x z hx ⋯
have mem₂ : ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
  (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x z hx sorry) (h₂ : p y z hy sorry), p (x * y) z sorry sorry
Tactic: induction hx using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
mem : ∀ (x : A) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : ∀ (r : R), p ((algebraMap R A : (a : R) → A) r) z ⋯ ⋯
mem₂ :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x z hx ⋯) (h₂ : p y z hy ⋯), p (x * y) z ⋯ ⋯
⊢ p x z hx ⋯
have mem₃ : ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
  (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x z hx sorry) (h₂ : p y z hy sorry), p (x + y) z sorry sorry
Tactic: induction hx using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
r : R
⊢ p x ((algebraMap R A : (a : R) → A) r) hx ⋯
have algebraMap : ∀ (x : A) (h : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) sorry sorry
Tactic: induction hx using adjoin_induction with
    | mem _ h => exact algebraMap_right _ _ h
    | algebraMap _ => exact algebraMap_both _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx