awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ((Algebra.algebraMap R A : (a : R) → A) r₁) ((Algebra.algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((Algebra.algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((Algebra.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
algebraMap : ∀ (x : A) (h : x ∈ s), p x ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
⊢ p x ((Algebra.algebraMap R A : (a : R) → A) r) hx ⋯
have algebraMap₁ : ∀ (r_1 : R), p ((Algebra.algebraMap R A : (a : R) → A) r_1) ((Algebra.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
-- 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 ((Algebra.algebraMap R A : (a : R) → A) r₁) ((Algebra.algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((Algebra.algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((Algebra.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
algebraMap : ∀ (x : A) (h : x ∈ s), p x ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
algebraMap₁ : ∀ (r_1 : R), p ((Algebra.algebraMap R A : (a : R) → A) r_1) ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
⊢ p x ((Algebra.algebraMap R A : (a : R) → A) r) hx ⋯
have algebraMap₂ : ∀ (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 ((Algebra.algebraMap R A : (a : R) → A) r) hx sorry)
  (h₂ : p y ((Algebra.algebraMap R A : (a : R) → A) r) hy sorry), p (x * y) ((Algebra.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
-- 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 ((Algebra.algebraMap R A : (a : R) → A) r₁) ((Algebra.algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((Algebra.algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((Algebra.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
algebraMap : ∀ (x : A) (h : x ∈ s), p x ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
algebraMap₁ : ∀ (r_1 : R), p ((Algebra.algebraMap R A : (a : R) → A) r_1) ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
algebraMap₂ :
  ∀ (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 ((Algebra.algebraMap R A : (a : R) → A) r) hx ⋯)
    (h₂ : p y ((Algebra.algebraMap R A : (a : R) → A) r) hy ⋯), p (x * y) ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
⊢ p x ((Algebra.algebraMap R A : (a : R) → A) r) hx ⋯
have algebraMap₃ : ∀ (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 ((Algebra.algebraMap R A : (a : R) → A) r) hx sorry)
  (h₂ : p y ((Algebra.algebraMap R A : (a : R) → A) r) hy sorry), p (x + y) ((Algebra.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
-- 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
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
⊢ p x y hx hy
have mem : ∀ (z : A) (hz : z ∈ s), p x z hx sorry
Tactic: induction hy using adjoin_induction with
  | mem z hz => 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₂
  | algebraMap r =>
    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₂
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- 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
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
mem : ∀ (z : A) (hz : z ∈ s), p x z hx ⋯
⊢ p x y hx hy
have algebraMap : ∀ (r : R), p x ((algebraMap R A : (a : R) → A) r) hx sorry
Tactic: induction hy using adjoin_induction with
  | mem z hz => 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₂
  | algebraMap r =>
    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₂
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- 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 ((Algebra.algebraMap R A : (a : R) → A) r₁) ((Algebra.algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((Algebra.algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((Algebra.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
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
mem : ∀ (z : A) (hz : z ∈ s), p x z hx ⋯
algebraMap : ∀ (r : R), p x ((Algebra.algebraMap R A : (a : R) → A) r) hx ⋯
⊢ p x y hx hy
have mul : ∀ (x_1 y : A) (hx_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1)
  (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
  p x (x_1 * y) hx sorry
Tactic: induction hy using adjoin_induction with
  | mem z hz => 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₂
  | algebraMap r =>
    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₂
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- 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 ((Algebra.algebraMap R A : (a : R) → A) r₁) ((Algebra.algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((Algebra.algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((Algebra.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
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
mem : ∀ (z : A) (hz : z ∈ s), p x z hx ⋯
algebraMap : ∀ (r : R), p x ((Algebra.algebraMap R A : (a : R) → A) r) hx ⋯
mul :
  ∀ (x_1 y : A) (hx_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
    p x (x_1 * y) hx ⋯
⊢ p x y hx hy
have add : ∀ (x_1 y : A) (hx_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1)
  (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
  p x (x_1 + y) hx sorry
Tactic: induction hy using adjoin_induction with
  | mem z hz => 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₂
  | algebraMap r =>
    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₂
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- 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
⊢ Eq (α := Subalgebra R ↥(adjoin R s))
    (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s)) ⊤
have refine_1 : ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (a : A) (ha : a ∈ s),
  Membership.mem (γ := Subalgebra R ↥(adjoin R s))
    (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) a sorry)
Tactic: refine eq_top_iff.2 fun ⟨x, hx⟩ ↦
      adjoin_induction (fun a ha ↦ ?_) (fun r ↦ ?_) (fun _ _ _ _ ↦ ?_) (fun _ _ _ _ ↦ ?_) 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
refine_1 :
  ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (a : A) (ha : a ∈ s),
    Membership.mem (γ := Subalgebra R ↥(adjoin R s))
      (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) a ⋯)
⊢ Eq (α := Subalgebra R ↥(adjoin R s))
    (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s)) ⊤
have refine_2 : ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (r : R),
  Membership.mem (α := ↥(adjoin R s)) (γ := Subalgebra R ↥(adjoin R s))
    (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
        ((algebraMap R A : (a : R) → A) r) sorry :
      ↥(adjoin R s))
Tactic: refine eq_top_iff.2 fun ⟨x, hx⟩ ↦
      adjoin_induction (fun a ha ↦ ?_) (fun r ↦ ?_) (fun _ _ _ _ ↦ ?_) (fun _ _ _ _ ↦ ?_) 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
refine_1 :
  ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (a : A) (ha : a ∈ s),
    Membership.mem (γ := Subalgebra R ↥(adjoin R s))
      (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) a ⋯)
refine_2 :
  ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (r : R),
    Membership.mem (α := ↥(adjoin R s)) (γ := Subalgebra R ↥(adjoin R s))
      (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
          ((algebraMap R A : (a : R) → A) r) ⋯ :
        ↥(adjoin R s))
⊢ Eq (α := Subalgebra R ↥(adjoin R s))
    (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s)) ⊤
have refine_3 : ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x x_1 : A)
  (x_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
  (x_3 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1),
  Membership.mem (γ := Subalgebra R ↥(adjoin R s))
      (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x x_2) →
    Membership.mem (γ := Subalgebra R ↥(adjoin R s))
        (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_1 x_3) →
      Membership.mem (γ := Subalgebra R ↥(adjoin R s))
        (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x + x_1) sorry)
Tactic: refine eq_top_iff.2 fun ⟨x, hx⟩ ↦
      adjoin_induction (fun a ha ↦ ?_) (fun r ↦ ?_) (fun _ _ _ _ ↦ ?_) (fun _ _ _ _ ↦ ?_) hx