awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
have h : Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ (n₂ + n₁) • x)
Tactic: use n₂ + n₁
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
⊢ OfLocalizationSpan @Finite
have rw : OfLocalizationFiniteSpan @Finite
Tactic: classical
  rw [RingHom.ofLocalizationSpan_iff_finite]
  introv R hs H
  -- We first setup the instances
  letI := f.toAlgebra
  letI := fun r : s => (Localization.awayMap f r).toAlgebra
  have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S))
      (Localization.Away (f r)) := by
    rw [Submonoid.map_powers]; exact Localization.isLocalization
  haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) :=
    fun r => IsScalarTower.of_algebraMap_eq'
      (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm
  -- By the hypothesis, we may find a finite generating set for each `Sᵣ`. This set can then be
  -- lifted into `R` by multiplying a sufficiently large power of `r`. I claim that the union of
  -- these generates `S`.
  constructor
  replace H := fun r => (H r).1
  choose s₁ s₂ using H
  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
  use s.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  -- It suffices to show that `r ^ n • x ∈ span T` for each `r : s`, since `{ r ^ n }` spans `R`.
  -- This then follows from the fact that each `x : R` is a linear combination of the generating set
  -- of `Sᵣ`. By multiplying a sufficiently large power of `r`, we can cancel out the `r`s in the
  -- denominators of both the generating set and the coefficients.
  rintro x -
  apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _
  intro r
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x)
      (by rw [s₂ r]; trivial)
  dsimp only at hn₁
  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
      (Localization.Away (f r)) _ (s₁ r) hn₁
  rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
  simp_rw [Submonoid.map_powers] at hn₂
  use n₂ + n₁
  exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
rw rw₁ rw₂ : OfLocalizationFiniteSpan @Finite
⊢ OfLocalizationSpan @Finite
have rw₃ : ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
  (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤)
  (H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))), f.Finite
Tactic: classical
  rw [RingHom.ofLocalizationSpan_iff_finite]
  introv R hs H
  -- We first setup the instances
  letI := f.toAlgebra
  letI := fun r : s => (Localization.awayMap f r).toAlgebra
  have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S))
      (Localization.Away (f r)) := by
    rw [Submonoid.map_powers]; exact Localization.isLocalization
  haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) :=
    fun r => IsScalarTower.of_algebraMap_eq'
      (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm
  -- By the hypothesis, we may find a finite generating set for each `Sᵣ`. This set can then be
  -- lifted into `R` by multiplying a sufficiently large power of `r`. I claim that the union of
  -- these generates `S`.
  constructor
  replace H := fun r => (H r).1
  choose s₁ s₂ using H
  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
  use s.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  -- It suffices to show that `r ^ n • x ∈ span T` for each `r : s`, since `{ r ^ n }` spans `R`.
  -- This then follows from the fact that each `x : R` is a linear combination of the generating set
  -- of `Sᵣ`. By multiplying a sufficiently large power of `r`, we can cancel out the `r`s in the
  -- denominators of both the generating set and the coefficients.
  rintro x -
  apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _
  intro r
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x)
      (by rw [s₂ r]; trivial)
  dsimp only at hn₁
  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
      (Localization.Away (f r)) _ (s₁ r) hn₁
  rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
  simp_rw [Submonoid.map_powers] at hn₂
  use n₂ + n₁
  exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (goal)
Goal:
⊢ IsStableUnderBaseChange @FinitePresentation
have h₁ : RespectsIso @FinitePresentation
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (goal)
Goal:
h₁ : RespectsIso @FinitePresentation
⊢ IsStableUnderBaseChange @FinitePresentation
have h₂ : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  FinitePresentation (algebraMap R T) → FinitePresentation (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (goal)
Goal:
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    FinitePresentation (algebraMap R T) → FinitePresentation (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have h₂ : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T], Algebra.FinitePresentation R T → Algebra.FinitePresentation S (S ⊗[R] T)
Tactic: simp only [finitePresentation_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ FinitePresentation (algebraMap R S)
have rw : Algebra.FinitePresentation R S
Tactic: rw [finitePresentation_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FinitePresentation R (Localization.Away r)
have h : Eq.{u_1 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring →
  Eq.{u_1 + 1} (α := Algebra R (Localization.Away r)) OreLocalization.instAlgebra
    (toAlgebra (comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f))
Tactic: convert! H ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_1 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring
⊢ Eq.{u_1 + 1} (α := Algebra R (Localization.Away r)) OreLocalization.instAlgebra
    (toAlgebra (comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f))
have h : ∀ (r_1 : R) (x : OreLocalization (Submonoid.powers r) S),
  (have I : Algebra R (OreLocalization (Submonoid.powers r) S) := OreLocalization.instAlgebra;
    r_1 • x) =
    r_1 • x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_1 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring
r_1 : R
x : OreLocalization (Submonoid.powers r) S
⊢ (have I : Algebra R (OreLocalization (Submonoid.powers r) S) := OreLocalization.instAlgebra;
    r_1 • x) =
    r_1 • x
have h : HMul.hMul (α := OreLocalization (Submonoid.powers r) S)
    ((algebraMap R (OreLocalization (Submonoid.powers r) S) : (a : R) → OreLocalization (Submonoid.powers r) S) r_1 :
      OreLocalization (Submonoid.powers r) S)
    x =
  r_1 • x
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FinitePresentation (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    FinitePresentation (B := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
⊢ f.FinitePresentation
have H₁ : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away r)
Tactic: replace H : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away (r : S)) := by
    intro r hr; simp_rw [RingHom.FinitePresentation] at H; convert! H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
⊢ RespectsIso @FiniteType
have refine : ∀ {R S : Type u_5} (x : CommRing R) (x_1 : CommRing S) (e : R ≃+* S), e.toRingHom.FiniteType
Tactic: refine finiteType_stableUnderComposition.respectsIso (fun {R S} _ _ e ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
⊢ IsStableUnderBaseChange @FiniteType
have h₁ : RespectsIso @FiniteType
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
h₁ : RespectsIso @FiniteType
⊢ IsStableUnderBaseChange @FiniteType
have h₂ : ∀ ⦃R S T : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T], FiniteType (algebraMap R T) → FiniteType (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (hypothesis)
Goal:
R S T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FiniteType (algebraMap R T)
⊢ FiniteType (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have h₁ : Algebra.FiniteType R T
Tactic: rw [finiteType_algebraMap] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
R S T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.FiniteType R T
⊢ FiniteType (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have h₂ : Algebra.FiniteType S (S ⊗[R] T)
Tactic: apply finiteType_algebraMap.mpr
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
⊢ OfLocalizationSpan @FiniteType
have refine : ∀ {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R)
  (hs : Eq (α := Ideal R) (Ideal.span s) ⊤)
  (h :
    ∀ r ∈ s,
      FiniteType.{u_5, u_5} (A := Localization.Away r) (B := Localization.Away r ⊗[R] S)
        (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))),
  FiniteType (algebraMap R S)
Tactic: refine OfLocalizationSpan.mk _ finiteType_respectsIso (fun s hs h ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
h :
  ∀ r ∈ s,
    FiniteType.{u_5, u_5} (A := Localization.Away r) (B := Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
⊢ FiniteType (algebraMap R S)
have simp_rw : ∀ (h : ∀ r ∈ s, Algebra.FiniteType.{u_5, u_5} (Localization.Away r) (Localization.Away r ⊗[R] S)),
  Algebra.FiniteType R S
Tactic: simp_rw [finiteType_algebraMap] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ FiniteType (algebraMap R S)
have rw : Algebra.FiniteType R S
Tactic: rw [finiteType_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FiniteType R (Localization.Away r)
have h : Eq.{u_5 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring →
  Eq.{u_5 + 1} (α := Algebra R (Localization.Away r)) OreLocalization.instAlgebra
    (toAlgebra (comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f))
Tactic: convert! H ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_5 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring
⊢ Eq.{u_5 + 1} (α := Algebra R (Localization.Away r)) OreLocalization.instAlgebra
    (toAlgebra (comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f))
have h : ∀ (r_1 : R) (x : OreLocalization (Submonoid.powers r) S),
  (have I : Algebra R (OreLocalization (Submonoid.powers r) S) := OreLocalization.instAlgebra;
    r_1 • x) =
    r_1 • x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_5 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring
r_1 : R
x : OreLocalization (Submonoid.powers r) S
⊢ (have I : Algebra R (OreLocalization (Submonoid.powers r) S) := OreLocalization.instAlgebra;
    r_1 • x) =
    r_1 • x
have h : HMul.hMul (α := OreLocalization (Submonoid.powers r) S)
    ((algebraMap R (OreLocalization (Submonoid.powers r) S) : (a : R) → OreLocalization (Submonoid.powers r) S) r_1 :
      OreLocalization (Submonoid.powers r) S)
    x =
  r_1 • x
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FiniteType (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_5)),
    FiniteType (B := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
⊢ f.FiniteType
have H₁ : ∀ r ∈ s, Algebra.FiniteType R (Localization.Away r)
Tactic: replace H : ∀ r ∈ s, Algebra.FiniteType R (Localization.Away (r : S)) := by
    intro r hr; simp_rw [RingHom.FiniteType] at H; convert! H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Flat (algebraMap R S) ↔ Module.Flat R S
have rw : Module.Flat R S ↔ Module.Flat R S
Tactic: rw [RingHom.Flat, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Module.Flat R S ↔ Module.Flat R S
⊢ Flat (algebraMap R S) ↔ Module.Flat R S
have rw₁ : Module.Flat R S ↔ Module.Flat R S
Tactic: rw [RingHom.Flat, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
⊢ (g.comp f).Flat
have algebraizeInst : Module.Flat R S
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
algebraizeInst : Module.Flat R S
⊢ (g.comp f).Flat
have algebraizeInst₁ : Module.Flat S T
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
⊢ RespectsIso.{u_4} fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ Flat
have apply : ∀ {R S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Flat
Tactic: apply stableUnderComposition.respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_4} fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ Flat
have apply : ∀ ⦃R S T : Type u_4⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T], Flat (algebraMap R T) → Flat (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
Tactic: apply IsStableUnderBaseChange.mk respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Flat (algebraMap R T)
⊢ Flat (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have rw : ∀ (h : Module.Flat R T), Module.Flat S (S ⊗[R] T)
Tactic: rw [flat_algebraMap_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h :
  ∀ (r : (↑s : Type u_4)),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop)) _ (Localization.Away (↑r : S)) _ _
      (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
⊢ f.Flat
have refine : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
Tactic: refine Module.flat_of_isLocalized_span _ _ s hsp _
    (fun r ↦ Algebra.linearMap S <| Localization.Away r.1) ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
⊢ ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
have h₁ : ∀ (a : (↑s : Type u_4)),
  Eq.{u_4 + 1} (α := Module R (Localization.Away (↑a : S)))
    (OreLocalization.instModuleOfIsScalarTower : Module R (OreLocalization (Submonoid.powers (↑a : S)) S))
    Algebra.toModule
Tactic: convert! h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
a : (↑s : Type u_4)
⊢ Eq.{u_4 + 1} (α := Module R (Localization.Away (↑a : S)))
    (OreLocalization.instModuleOfIsScalarTower : Module R (OreLocalization (Submonoid.powers (↑a : S)) S))
    Algebra.toModule
have h₁ : ∀ (x : R) (x_1 : OreLocalization (Submonoid.powers (↑a : S)) S), SMul.smul x x_1 = SMul.smul x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
⊢ Module.Flat R S
have apply : ∀ (P : Ideal S) [inst_2 : P.IsMaximal], Module.Flat R (Localization.AtPrime P)
Tactic: apply Module.flat_of_isLocalized_maximal S S (fun P ↦ Localization.AtPrime P)
    (fun P ↦ Algebra.linearMap S _)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
P : Ideal S
inst_2 : P.IsMaximal
algInst_1 : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
⊢ Module.Flat R (Localization.AtPrime P)
have this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
Tactic: have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm