awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) 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_2 h) →
    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_3 h_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_2 * x_3) ⋯)

Tactic:
Subalgebra.mul_mem _

Premises used: Subalgebra.mul_mem, Set.Mem
-- 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_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) 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_2 h) →
    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_3 h_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_2 * x_3) ⋯)

Tactic:
exact Subalgebra.mul_mem _

Premises used: Subalgebra.mul_mem
-- 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
⊢ Eq (α := Subalgebra R A) (adjoin R (s ∪ t)) (adjoin R s ⊔ adjoin R t)

Tactic:
(Algebra.gc : GaloisConnection _ ((↑) : Subalgebra R A → Set A)).l_sup

Premises used: GaloisConnection.l_sup, 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
⊢ Eq.{uA + 1} (α := Subalgebra R A) R[] ⊥

Tactic:
Algebra.gc.l_bot

Premises used: GaloisConnection.l_bot, 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
⊢ Eq.{uA + 1} (α := Subalgebra R A) (adjoin R Set.univ) ⊤

Tactic:
Algebra.gi.l_top

Premises used: Algebra.gi, GaloisInsertion.l_top
-- 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
x : R
⊢ Eq (α := Subalgebra R A) R[((algebraMap R A : (a : R) → A) x : A)] ⊥

Tactic:
bot_unique <| adjoin_singleton_le <| Subalgebra.algebraMap_mem _ _

Premises used: Algebra.adjoin_singleton_le, bot_unique, Subalgebra.algebraMap_mem
-- 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
n : ℕ
⊢ Eq (α := Subalgebra R A) R[(↑n : A)] ⊥

Tactic:
simpa using adjoin_singleton_algebraMap A (n : R)

Premises used: Algebra.adjoin_singleton_algebraMap, Nat.cast
-- 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
⊢ Eq (α := Subalgebra R A) R[0] ⊥

Tactic:
mod_cast adjoin_singleton_natCast R A 0

Premises used: congrArg, Algebra.adjoin, cast, Bot.bot, Algebra.adjoin_singleton_natCast, congrFun', Nat.cast_zero, Singleton.singleton, OfNat.ofNat, Eq.symm, Eq, Eq.trans
-- 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
⊢ Eq (α := Subalgebra R A) R[1] ⊥

Tactic:
mod_cast adjoin_singleton_natCast R A 1

Premises used: congrArg, Algebra.adjoin, cast, Bot.bot, Algebra.adjoin_singleton_natCast, congrFun', Singleton.singleton, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- 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
x : R
s : Set A
rw : Eq (α := Subalgebra R A) (R[((algebraMap R A : (a : R) → A) x : A)] ⊔ adjoin R s) (adjoin R s)
⊢ Eq (α := Subalgebra R A) (adjoin R (insert (α := A) ((algebraMap R A : (a : R) → A) x : A) s)) (adjoin R s)

Tactic:
rw [Set.insert_eq, adjoin_union]

Premises used: Set.insert_eq, Algebra.adjoin_union
-- 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
x : R
s : Set A
⊢ Eq (α := Subalgebra R A) (R[((algebraMap R A : (a : R) → A) x : A)] ⊔ adjoin R s) (adjoin R s)

Tactic:
simp
-- 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
n : ℕ
s : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R (insert (↑n : A) s)) (adjoin R s)

Tactic:
mod_cast adjoin_insert_algebraMap (n : R) s

Premises used: congrArg, Algebra.adjoin, cast, Algebra.adjoin_insert_algebraMap, Insert.insert, Nat.cast, congrFun', algebraMap.coe_natCast, Eq
-- 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 (insert 0 s)) (adjoin R s)

Tactic:
mod_cast adjoin_insert_natCast R 0 s

Premises used: Algebra.adjoin_insert_natCast, congrArg, Algebra.adjoin, cast, Insert.insert, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Eq.trans
-- 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 (insert 1 s)) (adjoin R s)

Tactic:
mod_cast adjoin_insert_natCast R 1 s

Premises used: Algebra.adjoin_insert_natCast, congrArg, Algebra.adjoin, cast, Insert.insert, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- 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
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)
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))
⊢ 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)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
r : A
hr :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) r
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
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) r

Tactic:
rcases Subsemiring.mem_closure_iff_exists_list.1 hr with ⟨L, HL, rfl⟩

Premises used: Subsemiring.mem_closure_iff_exists_list, Iff.mp, rfl
-- 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
HL :
  ∀ (t : List A),
    Membership.mem (γ := List (List A)) [] t →
      ∀ 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.sum (List.map List.prod []))

Tactic:
zero_mem _

Premises used: Set.Mem, List.sum, ZeroMemClass.zero_mem, List.foldr
-- 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
HL :
  ∀ (t : List A),
    Membership.mem (γ := List (List A)) [] t →
      ∀ 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.sum (List.map List.prod []))

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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
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:
?_
-- 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
L : List (List A)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
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
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod L).sum

Tactic:
induction L with
    | nil => exact zero_mem _
    | cons hd tl ih => ?_

Premises used: ZeroMemClass.zero_mem
-- 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
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
⊢ (∀ 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

Premises used: List.forall_mem_cons
-- 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
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
a :
  Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (hd.prod + (List.map List.prod tl).sum)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (List.map List.prod (hd :: tl)).sum

Tactic:
rw [List.map_cons, List.sum_cons]

Premises used: List.map_cons, List.sum_cons
-- 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
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)

Tactic:
Submodule.add_mem _ ?_ (ih HL.2)

Premises used: Set.Mem, And.right, Submodule.add_mem
-- 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
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
a : Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (hd.prod + (List.map List.prod tl).sum)

Tactic:
refine Submodule.add_mem _ ?_ (ih HL.2)

Premises used: And.right, Submodule.add_mem
-- 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
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
⊢ ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s

Tactic:
replace HL := HL.1
-- 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
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
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
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod

Tactic:
rcases this with ⟨z, r, hr, hzr⟩
-- 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
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
rw : Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) (z • r)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Submonoid.closure s) : Set A)) hd.prod

Tactic:
rw [← hzr]
-- 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
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)) (z • r)

Tactic:
smul_mem _ _ (subset_span hr)

Premises used: Set.Mem, Submodule.subset_span, Submodule.smul_mem
-- 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
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)) (z • r)

Tactic:
exact smul_mem _ _ (subset_span hr)

Premises used: Submodule.subset_span, Submodule.smul_mem
-- 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
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
a : ∃ (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

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)
-- 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
HL :
  ∀ (y : A),
    Membership.mem (γ := List A) [] y → 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 = List.prod []

Tactic:
⟨1, 1, (Submonoid.closure s).one_mem', one_smul _ _⟩

Premises used: one_smul, Submonoid.closure, Exists.intro, Submonoid.one_mem', OfNat.ofNat
-- 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
HL :
  ∀ (y : A),
    Membership.mem (γ := List A) [] y → 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 = List.prod []

Tactic:
exact ⟨1, 1, (Submonoid.closure s).one_mem', one_smul _ _⟩
-- 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
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:
?_
-- 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
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
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
⊢ ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = hd.prod

Tactic:
induction hd with
    | nil => exact ⟨1, 1, (Submonoid.closure s).one_mem', one_smul _ _⟩
    | cons hd tl ih => ?_
-- 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
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
⊢ 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

Premises used: List.forall_mem_cons
-- 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
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
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
⊢ ∃ (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⟩

Premises used: And.right
-- 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
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 : ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r
⊢ ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = (hd :: tl).prod

Tactic:
rw [List.prod_cons, ← hzr]

Premises used: List.prod_cons