awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Topology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
rw : IsHausdorff I R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R
rw₁ : T2Space R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R
rw₂ : T2Space R ∧ CompleteSpace R ↔ CompleteSpace R ∧ T2Space R
⊢ IsAdicComplete I R ↔ CompleteSpace R ∧ T2Space R
have rw₃ : CompleteSpace R ∧ T2Space R ↔ CompleteSpace R ∧ T2Space R
Tactic: rw [isAdicComplete_iff, hI.isHausdorff_iff, hI.isPrecomplete_iff, and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Topology (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsPrecomplete (R := S) (Ideal.map e I) S ↔ IsPrecomplete I R
have rw : CompleteSpace R ↔ CompleteSpace S
Tactic: rw [iff_comm, IsAdic.isPrecomplete_iff (by rfl), IsAdic.isPrecomplete_iff (by rfl)]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Topology (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsHausdorff (R := S) (Ideal.map e I) S ↔ IsHausdorff I R
have rw : T2Space R ↔ T2Space S
Tactic: rw [iff_comm, IsAdic.isHausdorff_iff rfl, IsAdic.isHausdorff_iff rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
⊢ Eq (α := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (Subalgebra.prod (adjoin R s) (adjoin R t))
have a : LE.le (α := Subalgebra R (A × B))
  (adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
  (Subalgebra.prod (adjoin R s) (adjoin R t))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a :
  LE.le (α := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (Subalgebra.prod (adjoin R s) (adjoin R t))
⊢ Eq (α := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (Subalgebra.prod (adjoin R s) (adjoin R t))
have a₁ : LE.le (α := Subalgebra R (A × B)) (Subalgebra.prod (adjoin R s) (adjoin R t))
  (adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
⊢ Membership.mem (γ := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (a, b)
have Ha : Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}))) (a, 0)
Tactic: have Ha : (a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inl_map_mul ha
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
Ha :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}))) (a, 0)
⊢ Membership.mem (γ := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (a, b)
have Hb : Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))) (0, b)
Tactic: have Hb : ((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
Ha :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}))) (a, 0)
Hb :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))) (0, b)
⊢ Membership.mem (γ := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (a, b)
have Ha₁ : (a, 0) ∈ P
Tactic: replace Ha : (a, (0 : B)) ∈ P := adjoin_mono Set.subset_union_left Ha
Cleared hypotheses: Ha
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
Hb :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))) (0, b)
Ha : (a, 0) ∈ P
⊢ Membership.mem (γ := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (a, b)
have Hb₁ : (0, b) ∈ P
Tactic: replace Hb : ((0 : A), b) ∈ P := adjoin_mono Set.subset_union_right Hb
Cleared hypotheses: Hb
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
⊢ Eq (α := Subalgebra S A) (adjoin S (↑(adjoin R s) : Set A)) (adjoin S s)
have apply : LE.le (α := Subalgebra S A) (adjoin S s) (adjoin S (↑(adjoin R s) : Set A))
Tactic: apply le_antisymm (adjoin_le _)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
apply : LE.le (α := Subalgebra S A) (adjoin S s) (adjoin S (↑(adjoin R s) : Set A))
⊢ Eq (α := Subalgebra S A) (adjoin S (↑(adjoin R s) : Set A)) (adjoin S s)
have apply₁ : (↑(adjoin R s) : Set A) ⊆ (↑(adjoin S s) : Set A)
Tactic: apply le_antisymm (adjoin_le _)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
⊢ Eq (α := Subalgebra R A) (Subalgebra.restrictScalars R (adjoin S s))
    (AlgHom.range (IsScalarTower.toAlgHom R S A) ⊔ adjoin R s)
have refine : LE.le (α := Subalgebra R A) (AlgHom.range (IsScalarTower.toAlgHom R S A)) (Subalgebra.restrictScalars R (adjoin S s))
Tactic: refine le_antisymm (fun _ hx ↦ adjoin_induction
    (fun x hx ↦ le_sup_right (α := Subalgebra R A) (subset_adjoin hx))
    (fun x ↦ le_sup_left (α := Subalgebra R A) ⟨x, rfl⟩)
    (fun _ _ _ _ ↦ add_mem) (fun _ _ _ _ ↦ mul_mem) <|
    (Subalgebra.mem_restrictScalars _).mp hx) (sup_le ?_ <| adjoin_le subset_adjoin)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
⊢ Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s ∪ t))
have this : Eq (α := Subalgebra R B) (Subalgebra.map (IsScalarTower.toAlgHom R A B) (adjoin R s))
  (Subalgebra.map (IsScalarTower.toAlgHom R A B) ⊤)
Tactic: have := congr_arg (Subalgebra.map (IsScalarTower.toAlgHom R A B)) hS
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
this :
  Eq (α := Subalgebra R B) (Subalgebra.map (IsScalarTower.toAlgHom R A B) (adjoin R s))
    (Subalgebra.map (IsScalarTower.toAlgHom R A B) ⊤)
⊢ Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s ∪ t))
have this₁ : Eq (α := Subalgebra R B) (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))
  (AlgHom.range (IsScalarTower.toAlgHom R A B))
Tactic: rw [Algebra.map_top, AlgHom.map_adjoin, IsScalarTower.coe_toAlgHom'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
this :
  Eq (α := Subalgebra R B) (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))
    (AlgHom.range (IsScalarTower.toAlgHom R A B))
⊢ Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s ∪ t))
have rw : Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
  (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s)))
    (adjoin (↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))) t))
Tactic: rw [adjoin_union_eq_adjoin_adjoin, this, ← IsScalarTower.adjoin_range_toAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
this :
  Eq (α := Subalgebra R B) (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))
    (AlgHom.range (IsScalarTower.toAlgHom R A B))
rw :
  Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s)))
      (adjoin (↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))) t))
⊢ Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s ∪ t))
have rw₁ : Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
  (Subalgebra.restrictScalars R (S := ↥(AlgHom.range (IsScalarTower.toAlgHom R A B)))
    (adjoin (↥(AlgHom.range (IsScalarTower.toAlgHom R A B))) t))
Tactic: rw [adjoin_union_eq_adjoin_adjoin, this, ← IsScalarTower.adjoin_range_toAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
this :
  Eq (α := Subalgebra R B) (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))
    (AlgHom.range (IsScalarTower.toAlgHom R A B))
rw :
  Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s)))
      (adjoin (↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))) t))
rw₁ :
  Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (Subalgebra.restrictScalars R (S := ↥(AlgHom.range (IsScalarTower.toAlgHom R A B)))
      (adjoin (↥(AlgHom.range (IsScalarTower.toAlgHom R A B))) t))
⊢ Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s ∪ t))
have rw₂ : Eq (α := Subalgebra R B)
  (Subalgebra.restrictScalars R (S := ↥(AlgHom.range (IsScalarTower.toAlgHom R A B)))
    (adjoin (↥(AlgHom.range (IsScalarTower.toAlgHom R A B))) t))
  (Subalgebra.restrictScalars R (S := ↥(AlgHom.range (IsScalarTower.toAlgHom R A B)))
    (adjoin (↥(AlgHom.range (IsScalarTower.toAlgHom R A B))) t))
Tactic: rw [adjoin_union_eq_adjoin_adjoin, this, ← IsScalarTower.adjoin_range_toAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
x : B
hx : Membership.mem (γ := Subalgebra R B) (adjoin R s) x
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, r ^ n • x ∈ B'
have hx₁ : Membership.mem (γ := Submodule R B)
  ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) (adjoin R s) : Submodule R B) x
Tactic: change x ∈ Subalgebra.toSubmodule (adjoin R s) at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
x : B
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
hx :
  Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) (adjoin R s) : Submodule R B) x
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, r ^ n • x ∈ B'
have hx₁ : ∃ (l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R),
  (Finsupp.linearCombination R (Subtype.val (p := fun (x : B) ↦ x ∈ (↑(Submonoid.closure s) : Set B))) :
        (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB) →₀ R) → B)
      l =
    x
Tactic: rw [adjoin_eq_span, Finsupp.mem_span_iff_linearCombination] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
x : B
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
hx :
  ∃ (l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R),
    (Finsupp.linearCombination R (Subtype.val (p := fun (x : B) ↦ x ∈ (↑(Submonoid.closure s) : Set B))) :
          (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB) →₀ R) → B)
        l =
      x
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, r ^ n • x ∈ B'
have rcases : ∀ (l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R),
  ∃ (n₀ : ℕ),
    ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
Tactic: rcases hx with ⟨l, rfl : (l.sum fun (i : Submonoid.closure s) (c : R) => c • (i : B)) = x⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
⊢ ∃ (n₀ : ℕ),
    ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
have choose : ∀ (n₁ : (x : ↥(Submonoid.closure s)) → ℕ)
  (n₂ :
    ∀ (x : ↥(Submonoid.closure s)),
      Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))),
  ∃ (n₀ : ℕ),
    ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
Tactic: choose n₁ n₂ using fun x : Submonoid.closure s => Submonoid.pow_smul_mem_closure_smul r s x.prop
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
⊢ ∃ (n₀ : ℕ),
    ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
have h : ∀ n ≥ l.support.sup n₁,
  HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
Tactic: use l.support.sup n₁
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
⊢ HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
have h : (l.sum fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) ∈ B'
Tactic: rw [Finsupp.smul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
⊢ (l.sum fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) ∈ B'
have h : ∀ c ∈ l.support,
  Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    ((fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) c
      ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) c))
Tactic: refine B'.toSubmodule.sum_mem ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
⊢ Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    ((fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) a
      ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a))
have this : n ≥ n₁ a
Tactic: have : n ≥ n₁ a := le_trans (Finset.le_sup ha) hn
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    (r ^ n •
      HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R) (↑a : B))
have h : Membership.mem (γ := Submodule R B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
  (HPow.hPow (α := B) ((algebraMap A B : (a : A) → B) r : B) (n - n₁ a) *
    HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R)
      (r ^ n₁ a • (↑a : B)))
Tactic: rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul, ←
    IsScalarTower.algebraMap_smul A (l a) (a : B), smul_smul (r ^ n₁ a), mul_comm, ← smul_smul,
    smul_def, map_pow, IsScalarTower.algebraMap_smul]