awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)
⊢ (t * s') • (y • a + z) = ((↑t : R) * y') • a + (↑s' : R) • t • z
have insert : t • s' • y • a + s' • t • z = (↑t : R) • ((↑s' : R) • y) • a + (↑s' : R) • t • z
Tactic: rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
x : N
s' : Finset N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
have empty : ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑∅ : Set N)) x),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (t • x)
Tactic: induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]
Cleared hypotheses: x, s', hs'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
x : N
s' : Finset N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
empty :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑∅ : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
have insert : ∀ (a : N) (s : Finset N),
  a ∉ s →
    ∀
      (hs :
        ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
          ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x))
      (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑(insert a s) : Set N)) x),
      ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑(insert a s) : Set N)) (t • x)
Tactic: induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]
Cleared hypotheses: x, s', hs'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
have obtain : ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
  (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
Tactic: classical
  obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx
  rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
  · exact ⟨t, Submodule.span_mono hss' ht⟩
  clear hx hss' s
  induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
obtain :
  ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
    (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
have obtain₁ : ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
  (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x) (t : ↥M)
  (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
Tactic: classical
  obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx
  rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
  · exact ⟨t, Submodule.span_mono hss' ht⟩
  clear hx hss' s
  induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
obtain :
  ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
    (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
obtain₁ :
  ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
    (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x) (t : ↥M)
    (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
have obtain₂ : ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
  (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
Tactic: classical
  obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx
  rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
  · exact ⟨t, Submodule.span_mono hss' ht⟩
  clear hx hss' s
  induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
obtain :
  ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
    (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
obtain₁ :
  ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
    (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x) (t : ↥M)
    (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
obtain₂ obtain₃ :
  ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
    (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
have obtain₄ : ∀ (s' : Finset N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
Tactic: classical
  obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx
  rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
  · exact ⟨t, Submodule.span_mono hss' ht⟩
  clear hx hss' s
  induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]
Cleared hypotheses: s, hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
R' : Type u_3
inst_2 : CommSemiring R'
inst_3 : Algebra R R'
inst_4 : Algebra R' S
inst_5 : Algebra R S
inst_6 : IsScalarTower R R' S
inst_7 : IsLocalization M R'
s : Set S
x : S
hx : Membership.mem (γ := Subalgebra R' S) (Algebra.adjoin R' s) x
⊢ ∃ (t : ↥M),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R s) : Submodule R S) (t • x)
have hx₁ : Membership.mem (γ := Submodule R' S)
  ((Subalgebra.toSubmodule : (a : Subalgebra R' S) → Submodule R' S) (Algebra.adjoin R' s) : Submodule R' S) x
Tactic: change x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s) at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
R' : Type u_3
inst_2 : CommSemiring R'
inst_3 : Algebra R R'
inst_4 : Algebra R' S
inst_5 : Algebra R S
inst_6 : IsScalarTower R R' S
inst_7 : IsLocalization M R'
s : Set S
x : S
hx :
  Membership.mem (γ := Submodule R' S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R' S) → Submodule R' S) (Algebra.adjoin R' s) : Submodule R' S) x
⊢ ∃ (t : ↥M),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R s) : Submodule R S) (t • x)
have simp_rw : ∀ (hx : Membership.mem (γ := Submodule R' S) (Submodule.span R' (↑(Submonoid.closure s) : Set S)) x),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R S) (Submodule.span R (↑(Submonoid.closure s) : Set S)) (t • x)
Tactic: simp_rw [Algebra.adjoin_eq_span] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
⊢ Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
have h : Eq (α := R →+* Sₚ) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) sorry) (algebraMap R Rₚ))
Tactic: apply IsLocalization.ringHom_ext M
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
⊢ Module.Finite Rₚ Sₚ
have this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) sorry)
Tactic: have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
      (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
this :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
⊢ Module.Finite Rₚ Sₚ
have obtain : ∀ (T : Finset S) (hT : Eq (α := Submodule R S) (Submodule.span R (↑T : Set S)) ⊤), Module.Finite Rₚ Sₚ
Tactic: obtain ⟨T, hT⟩ := hRS
Cleared hypotheses: hRS
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
T : Finset S
hT : Eq (α := Submodule R S) (Submodule.span R (↑T : Set S)) ⊤
⊢ Module.Finite Rₚ Sₚ
have h : Eq (α := Submodule Rₚ Sₚ) (Submodule.span Rₚ (↑(Finset.image (⇑(algebraMap S Sₚ) : (a : S) → Sₚ) T) : Set Sₚ)) ⊤
Tactic: use T.image (algebraMap S Sₚ)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
⊢ Module.Finite Rₚ Sₚ
have have : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) sorry)
Tactic: classical
  have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
      (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
  -- We claim that if `S` is generated by `T` as an `R`-module,
  -- then `S'` is generated by `T` as an `R'`-module.
  obtain ⟨T, hT⟩ := hRS
  use T.image (algebraMap S Sₚ)
  simpa using span_eq_top_localization_localization Rₚ M Sₚ hT
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
have :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
⊢ Module.Finite Rₚ Sₚ
have have₁ : ∀
  (this :
    Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
      (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) sorry)),
  Module.Finite Rₚ Sₚ
Tactic: classical
  have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
      (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
  -- We claim that if `S` is generated by `T` as an `R`-module,
  -- then `S'` is generated by `T` as an `R'`-module.
  obtain ⟨T, hT⟩ := hRS
  use T.image (algebraMap S Sₚ)
  simpa using span_eq_top_localization_localization Rₚ M Sₚ hT
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
have :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
have₁ :
  ∀
    (this :
      Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
        (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)),
    Module.Finite Rₚ Sₚ
have₂ :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
have₃ have₄ :
  ∀
    (this :
      Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
        (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)),
    Module.Finite Rₚ Sₚ
⊢ Module.Finite Rₚ Sₚ
have have₅ : ∀
  (this :
    Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
      (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) sorry))
  (T : Finset S) (hT : Eq (α := Submodule R S) (Submodule.span R (↑T : Set S)) ⊤), Module.Finite Rₚ Sₚ
Tactic: classical
  have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
      (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
  -- We claim that if `S` is generated by `T` as an `R`-module,
  -- then `S'` is generated by `T` as an `R'`-module.
  obtain ⟨T, hT⟩ := hRS
  use T.image (algebraMap S Sₚ)
  simpa using span_eq_top_localization_localization Rₚ M Sₚ hT
Cleared hypotheses: hRS