awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (goal)
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : EssFiniteType (algebraMap R T)
⊢ EssFiniteType (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
have rw : ∀ (h : Algebra.EssFiniteType R T), Algebra.EssFiniteType S (TensorProduct R S T)
Tactic: rw [essFiniteType_algebraMap] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (goal)
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ EssFiniteType (algebraMap R S)
have rw : Algebra.EssFiniteType R S
Tactic: rw [essFiniteType_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : f.EssFiniteType
⊢ EssFiniteType (R := IsLocalRing.ResidueField R) (S := IsLocalRing.ResidueField S) (IsLocalRing.ResidueField.map f)
have refine : EssFiniteType (S := IsLocalRing.ResidueField S)
  (RingHom.comp (β := IsLocalRing.ResidueField R) (IsLocalRing.ResidueField.map f) (IsLocalRing.residue R))
Tactic: refine .of_comp (IsLocalRing.residue R) ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : f.EssFiniteType
⊢ EssFiniteType (S := IsLocalRing.ResidueField S)
    (RingHom.comp (β := IsLocalRing.ResidueField R) (IsLocalRing.ResidueField.map f) (IsLocalRing.residue R))
have rw : EssFiniteType (S := IsLocalRing.ResidueField S) (RingHom.comp (IsLocalRing.residue S) f)
Tactic: rw [IsLocalRing.ResidueField.map_comp_residue]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Etale (algebraMap R S) ↔ Algebra.Etale R S
have rw : Algebra.Etale R S ↔ Algebra.Etale R S
Tactic: rw [RingHom.Etale, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.Etale R S ↔ Algebra.Etale R S
⊢ Etale (algebraMap R S) ↔ Algebra.Etale R S
have rw₁ : Algebra.Etale R S ↔ Algebra.Etale R S
Tactic: rw [RingHom.Etale, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
⊢ @Etale = fun (R : Type u_6) (S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦
    f.FormallyUnramified ∧ f.Smooth
have h : ∀ (x : Type u_6) (x_1 : Type u_5) (x_2 : CommRing x) (x_3 : CommRing x_1) (x_4 : x →+* x_1),
  x_4.Etale ↔ x_4.FormallyUnramified ∧ x_4.Smooth
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
x : Type u_6
x_1 : Type u_5
x_2 : CommRing x
x_3 : CommRing x_1
x_4 : x →+* x_1
⊢ x_4.Etale ↔ x_4.FormallyUnramified ∧ x_4.Smooth
have h : x_4.FormallyUnramified ∧ x_4.Smooth ↔ x_4.FormallyUnramified ∧ x_4.Smooth
Tactic: rw [etale_iff_formallyUnramified_and_smooth]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Etale
⊢ f.FormallyUnramified
have hf₁ : f.FormallyUnramified ∧ f.Smooth
Tactic: rw [etale_iff_formallyUnramified_and_smooth] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.Etale
have rw : f.FormallyUnramified ∧ f.Smooth
Tactic: rw [etale_iff_formallyUnramified_and_smooth]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale
have rw : IsStableUnderBaseChange.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
  (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
    inst_1
Tactic: rw [eq_formallyUnramified_and_smooth]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
⊢ PropertyIsLocal.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale
have rw : PropertyIsLocal.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
  (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
    inst_1
Tactic: rw [eq_formallyUnramified_and_smooth]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Etale (goal)
Goal:
⊢ StableUnderComposition.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale
have rw : StableUnderComposition.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
  (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
    inst_1
Tactic: rw [eq_formallyUnramified_and_smooth]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Module.FaithfullyFlat R S ↔ Module.FaithfullyFlat R S
have a : toAlgebra (algebraMap R S) = inst_2
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
⊢ f.Flat
have algebraizeInst : Module.FaithfullyFlat R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)
have rw : Module.FaithfullyFlat R S ↔
  Module.Flat R S ∧
    Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
Tactic: rw [← algebraMap_toAlgebra f, faithfullyFlat_algebraMap_iff, flat_algebraMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
⊢ Eq (α := (f : R →+* S) → Prop) FaithfullyFlat fun (f : R →+* S) ↦ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)
have h : ∀ (x : R →+* S), x.FaithfullyFlat ↔ x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
x : R →+* S
⊢ x.FaithfullyFlat ↔ x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x)
have h : x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x) ↔ x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x)
Tactic: rw [iff_flat_and_comap_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (hypothesis)
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
⊢ (g.comp f).FaithfullyFlat
have algebraizeInst : Module.FaithfullyFlat R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (hypothesis)
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
algebraizeInst : Module.FaithfullyFlat R S
⊢ (g.comp f).FaithfullyFlat
have algebraizeInst₁ : Module.FaithfullyFlat S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.FaithfullyFlat
have rw : f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)
Tactic: rw [iff_flat_and_comap_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)
have refine : ∀ (p : PrimeSpectrum R), ∃ (a : PrimeSpectrum S), PrimeSpectrum.comap f a = p
Tactic: refine ⟨.of_bijective hf, fun p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : PrimeSpectrum R
⊢ ∃ (a : PrimeSpectrum S), PrimeSpectrum.comap f a = p
have h : PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) p) = p
Tactic: use p.comap ((RingEquiv.ofBijective f hf).symm : _ →+* _)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : PrimeSpectrum R
⊢ comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R
have a : ∀ (x : R),
  Eq (α := R) ((comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f : (a : R) → R) x : R)
    ((id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : PrimeSpectrum R
⊢ PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) p) = p
have this : comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R
Tactic: have : ((RingEquiv.ofBijective f hf).symm : _ →+* _).comp f = id R := by
    ext
    exact (RingEquiv.ofBijective f hf).injective (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : PrimeSpectrum R
this : comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R
⊢ PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) p) = p
have h : PrimeSpectrum.comap (comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f) p = p
Tactic: rw [← PrimeSpectrum.comap_comp_apply, this, PrimeSpectrum.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : PrimeSpectrum R
this : comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R
h : PrimeSpectrum.comap (comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f) p = p
⊢ PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) p) = p
have h₁ : PrimeSpectrum.comap (id R) p = p
Tactic: rw [← PrimeSpectrum.comap_comp_apply, this, PrimeSpectrum.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : PrimeSpectrum R
this : comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R
h : PrimeSpectrum.comap (comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f) p = p
h₁ : PrimeSpectrum.comap (id R) p = p
⊢ PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) p) = p
have h₂ : (fun (x : PrimeSpectrum R) ↦ x) p = p
Tactic: rw [← PrimeSpectrum.comap_comp_apply, this, PrimeSpectrum.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have algebraizeInst : Module.FaithfullyFlat R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FaithfullyFlat
have refine : ∀ (R S T : Type u_3) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T),
  FaithfullyFlat (algebraMap R T) → FaithfullyFlat (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
Tactic: refine .mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.FaithfullyFlat (goal)
Goal:
R S T : Type u_3
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R T)
⊢ FaithfullyFlat (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
have rw : Module.FaithfullyFlat R T → Module.FaithfullyFlat S (TensorProduct R S T)
Tactic: rw [faithfullyFlat_algebraMap_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
⊢ RespectsIso @Finite
have apply : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Finite
Tactic: apply finite_stableUnderComposition.respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
⊢ IsStableUnderBaseChange @Finite
have refine : ∀ ⦃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], Finite (algebraMap R T) → Finite (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
Tactic: refine IsStableUnderBaseChange.mk finite_respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (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], Finite (algebraMap R T) → Finite (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have simp : ∀ ⦃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], Module.Finite R T → Module.Finite S (S ⊗[R] T)
Tactic: simp only [finite_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this : Algebra R' S' := f'.toAlgebra
⊢ Finite (A := R') (IsLocalization.map S' f ⋯)
have this₁ : IsScalarTower R R' S'
Tactic: have : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq'
    (IsLocalization.map_comp M.le_comap_map).symm
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this : IsScalarTower R R' S'
⊢ Finite (A := R') (IsLocalization.map S' f ⋯)
have this₁ : IsScalarTower R S S'
Tactic: have : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' rfl
-- 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
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) S'
have rwa : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
Tactic: rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ Finite (A := R') (IsLocalization.map S' f ⋯)
have this₁ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
Tactic: have : IsLocalization (Algebra.algebraMapSubmonoid S M) S' := by
    rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this_5 : IsScalarTower R S S'
this : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
⊢ Finite (A := R') (IsLocalization.map S' f ⋯)
have this₁ : Module.Finite R S
Tactic: have : Module.Finite R S := hf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
⊢ OfLocalizationSpan @Finite
have rw : OfLocalizationFiniteSpan @Finite
Tactic: rw [RingHom.ofLocalizationSpan_iff_finite]
-- 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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
this_1 : Algebra R S := f.toAlgebra
this : (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))
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))
have rw : IsLocalization (R := S) (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R)) : Submonoid S)
  (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
Tactic: rw [Submonoid.map_powers]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
this_1 : Algebra R S := f.toAlgebra
this : (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))
⊢ f.Finite
have this₁ : ∀ (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))
Tactic: have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S))
      (Localization.Away (f r)) := by
    rw [Submonoid.map_powers]; exact Localization.isLocalization
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : 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 :
  ∀ (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))
⊢ f.Finite
have this₁ : ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
Tactic: 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
-- 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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : 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))
⊢ f.Finite
have fg_top : Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : 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))
⊢ Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
have H₁ : ∀ (r : ↥s),
  Submodule.FG.{u_5, u_5} (R := Localization.Away (↑r : R)) (M :=
    Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) ⊤
Tactic: replace H := fun r => (H r).1
Cleared hypotheses: H