awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
⊢ ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
    Algebra.FinitePresentation R S') (f : S' →ₐ[R] S),
    Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
have obtain : ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
  ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
    Algebra.FinitePresentation R S') (f : S' →ₐ[R] S),
    Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
Tactic: classical
  obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance
  suffices h : ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S')
      (f : S' →ₐ[R] S), (s : Set S) ⊆ AlgHom.range f by
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := h
    have hf : Function.Surjective f := by
      have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
      rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
    use S', ‹_›, ‹_›, ‹_›, ‹_›, ‹_›, f
  clear hs
  induction s using Finset.induction with
  | empty =>
    exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
  | insert a s has IH =>
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
    have ha := Algebra.IsIntegral.isIntegral (R := R) a
    have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
    have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
    algebraize [f.toRingHom]
    refine ⟨AdjoinRoot ((minpoly R a).map (algebraMap R S')), inferInstance, inferInstance,
      .trans S' _, .trans (S := S'), .trans _ S' _,
      (AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) a
        (by simp [← Polynomial.aeval_def])).restrictScalars R, ?_⟩
    simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]
    exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
      Algebra.FinitePresentation R S') (f : S' →ₐ[R] S),
      Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
    Algebra.FinitePresentation R S') (f : S' →ₐ[R] S),
    Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
have obtain₁ : ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
  ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
    Algebra.FinitePresentation R S') (f : S' →ₐ[R] S), (↑s : Set S) ⊆ (↑f.range : Set S)
Tactic: classical
  obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance
  suffices h : ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S')
      (f : S' →ₐ[R] S), (s : Set S) ⊆ AlgHom.range f by
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := h
    have hf : Function.Surjective f := by
      have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
      rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
    use S', ‹_›, ‹_›, ‹_›, ‹_›, ‹_›, f
  clear hs
  induction s using Finset.induction with
  | empty =>
    exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
  | insert a s has IH =>
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
    have ha := Algebra.IsIntegral.isIntegral (R := R) a
    have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
    have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
    algebraize [f.toRingHom]
    refine ⟨AdjoinRoot ((minpoly R a).map (algebraMap R S')), inferInstance, inferInstance,
      .trans S' _, .trans (S := S'), .trans _ S' _,
      (AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) a
        (by simp [← Polynomial.aeval_def])).restrictScalars R, ?_⟩
    simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]
    exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
      Algebra.FinitePresentation R S') (f : S' →ₐ[R] S),
      Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
obtain₁ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
      Algebra.FinitePresentation R S') (f : S' →ₐ[R] S), (↑s : Set S) ⊆ (↑f.range : Set S)
⊢ ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
    Algebra.FinitePresentation R S') (f : S' →ₐ[R] S),
    Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
have obtain₂ : ∀ (s : Finset S),
  ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ :
    Algebra.FinitePresentation R S') (f : S' →ₐ[R] S), (↑s : Set S) ⊆ (↑f.range : Set S)
Tactic: classical
  obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance
  suffices h : ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S')
      (f : S' →ₐ[R] S), (s : Set S) ⊆ AlgHom.range f by
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := h
    have hf : Function.Surjective f := by
      have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
      rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
    use S', ‹_›, ‹_›, ‹_›, ‹_›, ‹_›, f
  clear hs
  induction s using Finset.induction with
  | empty =>
    exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
  | insert a s has IH =>
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
    have ha := Algebra.IsIntegral.isIntegral (R := R) a
    have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
    have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
    algebraize [f.toRingHom]
    refine ⟨AdjoinRoot ((minpoly R a).map (algebraMap R S')), inferInstance, inferInstance,
      .trans S' _, .trans (S := S'), .trans _ S' _,
      (AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) a
        (by simp [← Polynomial.aeval_def])).restrictScalars R, ?_⟩
    simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]
    exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
⊢ FinitePresentation R S
have obtain : ∀ (S' : Type u) (w : CommRing S') (w_1 : Algebra R S'),
  Module.Finite R S' →
    Module.Free R S' →
      FinitePresentation R S' →
        ∀ (f : S' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)),
          FinitePresentation R S
Tactic: obtain ⟨S', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Module.Free R S'
w_4 : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ FinitePresentation R S
have refine : Ideal.FG (RingHom.ker f.toRingHom)
Tactic: refine .of_surjective hf ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Module.Free R S'
w_4 : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have apply : Submodule.FG (Submodule.restrictScalars R (RingHom.ker f.toRingHom))
Tactic: apply Submodule.FG.of_restrictScalars R
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
⊢ FinitePresentation R S
have obtain : ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
  Module.Finite R R' →
    Free R R' →
      Algebra.FinitePresentation R R' →
        ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
          FinitePresentation R S
Tactic: obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (hypothesis)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this : Algebra R' S := f.toAlgebra
⊢ FinitePresentation R S
have this₁ : IsScalarTower R R' S
Tactic: have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (hypothesis)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this_1 : Algebra R' S := f.toAlgebra
this : IsScalarTower R R' S
⊢ FinitePresentation R S
have this₁ : FinitePresentation R R'
Tactic: have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (hypothesis)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this_1 : Algebra R' S := f.toAlgebra
this_2 : IsScalarTower R R' S
this : FinitePresentation R R'
⊢ FinitePresentation R S
have this₁ : FinitePresentation R' S
Tactic: have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
⊢ FinitePresentation R S
have obtain : ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
  Module.Finite R R' →
    Free R R' →
      Algebra.FinitePresentation R R' →
        ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
          FinitePresentation R S
Tactic: classical
  obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
  letI := f.toRingHom.toAlgebra
  have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
  have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
  exact .trans R S R'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
obtain :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
obtain₁ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
⊢ FinitePresentation R S
have obtain₂ : ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
  Module.Finite R R' →
    Free R R' →
      Algebra.FinitePresentation R R' →
        ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
          let this := f.toAlgebra;
          ∀ (this : IsScalarTower R R' S), FinitePresentation R S
Tactic: classical
  obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
  letI := f.toRingHom.toAlgebra
  have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
  have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
  exact .trans R S R'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
obtain :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
obtain₁ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
obtain₂ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            let this := f.toAlgebra;
            ∀ (this : IsScalarTower R R' S), FinitePresentation R S
⊢ FinitePresentation R S
have obtain₃ : ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
  Module.Finite R R' →
    Free R R' →
      Algebra.FinitePresentation R R' →
        ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
          let this := f.toAlgebra;
          ∀ (this : IsScalarTower R R' S) (this : FinitePresentation R R'), FinitePresentation R S
Tactic: classical
  obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
  letI := f.toRingHom.toAlgebra
  have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
  have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
  exact .trans R S R'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.ModuleFinitePresentation (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
obtain :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
obtain₁ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
obtain₂ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            let this := f.toAlgebra;
            ∀ (this : IsScalarTower R R' S), FinitePresentation R S
obtain₃ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            let this := f.toAlgebra;
            ∀ (this : IsScalarTower R R' S) (this : FinitePresentation R R'), FinitePresentation R S
⊢ FinitePresentation R S
have obtain₄ : ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
  Module.Finite R R' →
    Free R R' →
      Algebra.FinitePresentation R R' →
        ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
          let this := f.toAlgebra;
          ∀ (this_1 : IsScalarTower R R' S) (this_2 : FinitePresentation R R') (this : FinitePresentation R' S),
            FinitePresentation R S
Tactic: classical
  obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
  letI := f.toRingHom.toAlgebra
  have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
  have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
  exact .trans R S R'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
have hn₁ : ∃ (S : Set M), S.Finite ∧ span R S = N
Tactic: rw [fg_def] at hn
Cleared hypotheses: hn, hin
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn : ∃ (S : Set M), S.Finite ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
have rcases : ∀ (s : Set M) (hfs : s.Finite) (hs : span R s = N), ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
Tactic: rcases hn with ⟨s, hfs, hs⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)
have refine_1 : HSub.hSub (α := R) 1 1 ∈ I
Tactic: refine ⟨1, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
refine_1 : HSub.hSub (α := R) 1 1 ∈ I
⊢ ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)
have refine_2 : N ≤
  comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1)
    (HSMul.hSMul (β := Submodule R M) I (span R s))
Tactic: refine ⟨1, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
refine_1 : HSub.hSub (α := R) 1 1 ∈ I
refine_2 :
  N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1)
      (HSMul.hSMul (β := Submodule R M) I (span R s))
⊢ ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)
have refine_3 : s ⊆ (↑N : Set M)
Tactic: refine ⟨1, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ HSub.hSub (α := R) 1 1 ∈ I
have refine_1 : 0 ∈ I
Tactic: rw [sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1)
      (HSMul.hSMul (β := Submodule R M) I (span R s))
have refine_2 : N ≤ comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1) (I • N)
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ Membership.mem (α := M) (I • N) (((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1 : (a : M) → M) n : M)
have refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n ∈ I • N
Tactic: change (1 : R) • n ∈ I • N
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n ∈ I • N
have refine_2 : n ∈ I • N
Tactic: rw [one_smul]