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
x : R
s : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R (insert (α := A) ((algebraMap R A : (a : R) → A) x : A) s)) (adjoin R s)
have rw : Eq (α := Subalgebra R A) (R[((algebraMap R A : (a : R) → A) x : A)] ⊔ adjoin R s) (adjoin R s)
Tactic: rw [Set.insert_eq, adjoin_union]
-- 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 (α := Submodule R A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
    (span R (↑(Submonoid.closure s) : Set A) : Submodule R A)
have a : LE.le (α := Submodule R A)
  ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
  (span R (↑(Submonoid.closure s) : Set A) : Submodule R A)
Tactic: apply le_antisymm
-- 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
a :
  LE.le (α := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
    (span R (↑(Submonoid.closure s) : Set A) : Submodule R A)
⊢ Eq (α := Submodule R A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
    (span R (↑(Submonoid.closure s) : Set A) : Submodule R A)
have a₁ : LE.le (α := Submodule R A) (span R (↑(Submonoid.closure s) : Set A))
  ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
Tactic: apply le_antisymm
-- 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
r : A
hr :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) r
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) r
have a : ∀ (L : List (List A)) (HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
  (hr :
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
      (List.map List.prod L).sum),
  Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod L).sum
Tactic: rcases Subsemiring.mem_closure_iff_exists_list.1 hr with ⟨L, HL, rfl⟩
Cleared hypotheses: r, hr
-- 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
L : List (List A)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod L).sum
have a : ∀ (hd : List A) (tl : List (List A))
  (ih :
    ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
      Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod tl).sum)
  (HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
  Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod (hd :: tl)).sum
Tactic: induction L with
    | nil => exact zero_mem _
    | cons hd tl ih => ?_
Cleared hypotheses: L, HL
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod tl).sum
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod (hd :: tl)).sum
have HL₁ : (∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s) ∧
  ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
Tactic: rw [List.forall_mem_cons] at HL
Cleared hypotheses: HL
-- 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
hd : List A
tl : List (List A)
ih :
  ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod tl).sum
HL :
  (∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s) ∧
    ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod (hd :: tl)).sum
have a : Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (hd.prod + (List.map List.prod tl).sum)
Tactic: rw [List.map_cons, List.sum_cons]
-- 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
hd : List A
tl : List (List A)
ih :
  ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod tl).sum
HL :
  (∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s) ∧
    ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (hd.prod + (List.map List.prod tl).sum)
have a : Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod
Tactic: refine Submodule.add_mem _ ?_ (ih HL.2)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod tl).sum
HL :
  (∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s) ∧
    ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod
have HL₁ : ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
Tactic: replace HL := HL.1
Cleared hypotheses: HL
-- 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
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
this : ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = hd.prod
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod
have rcases : ∀ (z : R) (r : A) (hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r) (hzr : z • r = hd.prod),
  Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod
Tactic: rcases this with ⟨z, r, hr, hzr⟩
Cleared hypotheses: this
-- 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
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = hd.prod
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod
have rw : Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (z • r)
Tactic: rw [← hzr]
-- 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
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod
have a : ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = hd.prod
Tactic: suffices ∃ (z r : _) (_hr : r ∈ Submonoid.closure s), z • r = List.prod hd by
      rcases this with ⟨z, r, hr, hzr⟩
      rw [← hzr]
      exact smul_mem _ _ (subset_span hr)
-- 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
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = hd.prod
have a : ∀ (hd : A) (tl : List A)
  (ih :
    ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
      ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod)
  (HL : ∀ y ∈ hd :: tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
  ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = (hd :: tl).prod
Tactic: induction hd with
    | nil => exact ⟨1, 1, (Submonoid.closure s).one_mem', one_smul _ _⟩
    | cons hd tl ih => ?_
Cleared hypotheses: hd, HL
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL : ∀ y ∈ hd :: tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = (hd :: tl).prod
have HL₁ : hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
  ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
Tactic: rw [List.forall_mem_cons] at HL
Cleared hypotheses: HL
-- 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
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL :
  hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = (hd :: tl).prod
have a : ∀ (z : R) (r : A) (hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r) (hzr : z • r = tl.prod),
  ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = (hd :: tl).prod
Tactic: rcases ih HL.2 with ⟨z, r, hr, hzr⟩
-- 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
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL :
  hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
⊢ ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = (hd :: tl).prod
have a : ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r
Tactic: rw [List.prod_cons, ← hzr]
-- 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
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL :
  hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r
have a : ∀ (hd : R)
  (HL :
    Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
        ((algebraMap R A : (a : R) → A) hd : A) ∧
      ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
  ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1),
    z_1 • r_1 = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
Tactic: rcases HL.1 with (⟨hd, rfl⟩ | hs)
Cleared hypotheses: hd, HL
-- 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
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL :
  hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
a :
  ∀ (hd : R)
    (HL :
      Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
          ((algebraMap R A : (a : R) → A) hd : A) ∧
        ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1),
      z_1 • r_1 = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r
have a₁ : ∀ (hs : hd ∈ s),
  ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r
Tactic: rcases HL.1 with (⟨hd, rfl⟩ | hs)
-- 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
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1),
    z_1 • r_1 = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
have a : (hd * z) • r = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
Tactic: refine ⟨hd * z, r, hr, ?_⟩
-- 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
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ (hd * z) • r = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
have a : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.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
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
a :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
⊢ (hd * z) • r = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
have a₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.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
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
a :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
a₁ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
⊢ (hd * z) • r = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
have a₂ : HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) hd : A) ((algebraMap R A : (a : R) → A) z : A) * r =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.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
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
a :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
a₁ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
a₂ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) hd : A) ((algebraMap R A : (a : R) → A) z : A) * r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
⊢ (hd * z) • r = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
have a₃ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r) =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.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
⊢ LE.le (α := Submodule R A) (span R (↑(Submonoid.closure s) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
have a : (↑(Submonoid.closure s) : Set A) ⊆
  (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) : Set A)
Tactic: refine span_le.2 ?_
-- 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
t : Submodule R A
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) ≤ t ↔
    (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)
have rw : span R (↑(Submonoid.closure s) : Set A) ≤ t ↔ (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)
Tactic: rw [adjoin_eq_span, span_le]
-- 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
t : Submodule R A
rw : span R (↑(Submonoid.closure s) : Set A) ≤ t ↔ (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) ≤ t ↔
    (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)
have rw₁ : (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A) ↔ (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)
Tactic: rw [adjoin_eq_span, span_le]