awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
h' : I ≤ J.radical
h : I.FG
⊢ ∃ (n : ℕ), I ^ n ≤ J
have singleton : ∀ (x : R) (h' : R ∙ x ≤ J.radical), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J
Tactic: induction I, h using Submodule.fg_induction with
  | singleton x =>
    simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at h'
    obtain ⟨n, hn⟩ := h'
    refine ⟨n, by simpa [span_singleton_pow, span_le]⟩
  | sup I₁ I₂ _ _ h₁ h₂ =>
    obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans h')
    obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans h')
    use n₁ + n₂
    exact sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)
Cleared hypotheses: h', h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
h' : I ≤ J.radical
h : I.FG
singleton : ∀ (x : R) (h' : R ∙ x ≤ J.radical), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J
⊢ ∃ (n : ℕ), I ^ n ≤ J
have sup : ∀ (I₁ I₂ : Submodule R R),
  I₁.FG →
    I₂.FG →
      ∀ (h₁ : ∀ (h' : I₁ ≤ J.radical), ∃ (n : ℕ), I₁ ^ n ≤ J) (h₂ : ∀ (h' : I₂ ≤ J.radical), ∃ (n : ℕ), I₂ ^ n ≤ J)
        (h' : I₁ ⊔ I₂ ≤ J.radical), ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
Tactic: induction I, h using Submodule.fg_induction with
  | singleton x =>
    simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at h'
    obtain ⟨n, hn⟩ := h'
    refine ⟨n, by simpa [span_singleton_pow, span_le]⟩
  | sup I₁ I₂ _ _ h₁ h₂ =>
    obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans h')
    obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans h')
    use n₁ + n₂
    exact sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)
Cleared hypotheses: h', h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
N : Submodule R M
hI : I.FG
hN : N.FG
⊢ (I • N).FG
have obtain : ∀ (s : Finset R) [IsTwoSided (span (↑s : Set R))], (HSMul.hSMul (α := Ideal R) (span (↑s : Set R)) N).FG
Tactic: obtain ⟨s, rfl⟩ := hI
Cleared hypotheses: I, inst_3, hI
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
hN : N.FG
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
⊢ (HSMul.hSMul (α := Ideal R) (span (↑s : Set R)) N).FG
have obtain : ∀ (t : Finset M),
  (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (span (↑s : Set R)) (Submodule.span R (↑t : Set M))).FG
Tactic: obtain ⟨t, rfl⟩ := hN
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
t : Finset M
⊢ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (span (↑s : Set R)) (Submodule.span R (↑t : Set M))).FG
have rw : Submodule.FG (Submodule.span R (↑(s • t) : Set M))
Tactic: rw [Submodule.span_smul_span, ← s.coe_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
t : Finset M
⊢ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (span (↑s : Set R)) (Submodule.span R (↑t : Set M))).FG
have classical : Submodule.FG (Submodule.span R (↑(s • t) : Set M))
Tactic: classical rw [Submodule.span_smul_span, ← s.coe_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ (I ^ Nat.zero).FG
have rw : FG.{u_1} (R := R) ⊤
Tactic: rw [I.pow_zero, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n_1 : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I ^ n.succ).FG
have rw : (I * I ^ n).FG
Tactic: rw [IsTwoSided.pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Lattice (goal)
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Sort u_1
inst_3 : Finite ι
S : ι → Submodule R V
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
⊢ Module.Finite.{u_2, u_3} R ↥(⨆ (i : ι), S i)
have intro : ∀ (val : Fintype (PLift ι)), Module.Finite.{u_2, u_3} R ↥(⨆ (i : ι), S i)
Tactic: cases nonempty_fintype (PLift ι)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Lattice (goal)
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Sort u_1
inst_3 : Finite ι
S : ι → Submodule R V
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
val : Fintype (PLift ι)
⊢ Module.Finite.{u_2, u_3} R ↥(⨆ (i : ι), S i)
have intro : Module.Finite.{u_2, u_3} R ↥(Finset.sup Finset.univ fun (i : PLift ι) ↦ S i.down)
Tactic: rw [← iSup_plift_down, ← Finset.sup_univ_eq_iSup]
-- 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: obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance
-- 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 : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
h :
  ∃ (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' : Type u) (w : CommRing S') (w_1 : Algebra R S'),
  Module.Finite R S' →
    Free R S' →
      Algebra.FinitePresentation R S' →
        ∀ (f : S' →ₐ[R] S) (hsf : (↑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)
Tactic: obtain ⟨S', _, _, _, _, _, f, hsf⟩ := h
Cleared hypotheses: h
-- 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
s : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
⊢ Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
have this : Submodule.span R (↑s : Set S) ≤ f.toLinearMap.range
Tactic: have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
-- 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 : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
this : Submodule.span R (↑s : Set S) ≤ f.toLinearMap.range
⊢ Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
have rwa : ∀ (this : ⊤ ≤ f.toLinearMap.range), Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
Tactic: rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
Cleared hypotheses: this
-- 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 : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
this : Submodule.span R (↑s : Set S) ≤ f.toLinearMap.range
rwa : ∀ (this : ⊤ ≤ f.toLinearMap.range), Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
have rwa₁ : ∀ (this : f.toLinearMap.range = ⊤), Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
Tactic: rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
Cleared hypotheses: this
-- 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 : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
this : Submodule.span R (↑s : Set S) ≤ f.toLinearMap.range
rwa : ∀ (this : ⊤ ≤ f.toLinearMap.range), Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
rwa₁ : ∀ (this : f.toLinearMap.range = ⊤), Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
have rwa₂ : ∀ (this : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f.toLinearMap : (a : S') → S)),
  Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
Tactic: rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
Cleared hypotheses: this
-- 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
s : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑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 hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
Tactic: 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
-- 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 : 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)
have suffices : ∃ (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: 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
-- 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
a : S
s : Finset S
has : a ∉ s
IH :
  ∃ (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), (↑(insert a s) : Set S) ⊆ (↑f.range : Set S)
have insert : ∀ (S' : Type u) (w : CommRing S') (w_1 : Algebra R S'),
  Module.Finite R S' →
    Free R S' →
      Algebra.FinitePresentation R S' →
        ∀ (f : S' →ₐ[R] S) (hsf : (↑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), (↑(insert a s) : Set S) ⊆ (↑f.range : Set S)
Tactic: obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
Cleared hypotheses: IH
-- 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
a : S
s : Finset S
has : a ∉ s
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑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), (↑(insert a s) : Set S) ⊆ (↑f.range : Set S)
have ha : IsIntegral R a
Tactic: have ha := Algebra.IsIntegral.isIntegral (R := R) a
-- 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
a : S
s : Finset S
has : a ∉ s
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
ha : IsIntegral R a
⊢ ∃ (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), (↑(insert a s) : Set S) ⊆ (↑f.range : Set S)
have this : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
Tactic: have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
-- 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
a : S
s : Finset S
has : a ∉ s
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
ha : IsIntegral R a
this : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
⊢ ∃ (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), (↑(insert a s) : Set S) ⊆ (↑f.range : Set S)
have this₁ : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
Tactic: have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
-- 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
a : S
s : Finset S
has : a ∉ s
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
ha : IsIntegral R a
this_1 : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
this : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
algInst : Algebra S' S := f.toAlgebra
⊢ ∃ (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), (↑(insert a s) : Set S) ⊆ (↑f.range : Set S)
have insert : (↑(insert a s) : Set S) ⊆
  (↑(AlgHom.range (A := AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
        (AlgHom.restrictScalars R
          (AdjoinRoot.liftAlgHom (Polynomial.map (algebraMap R S') (minpoly R a)) (Algebra.ofId S' S) a sorry))) :
    Set S)
Tactic: 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, ?_⟩
-- 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
a : S
s : Finset S
has : a ∉ s
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Free R S'
w_4 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
ha : IsIntegral R a
this_1 : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
this : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
algInst : Algebra S' S := f.toAlgebra
⊢ (↑(insert a s) : Set S) ⊆
    (↑(AlgHom.range (A := AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
          (AlgHom.restrictScalars R
            (AdjoinRoot.liftAlgHom (Polynomial.map (algebraMap R S') (minpoly R a)) (Algebra.ofId S' S) a ⋯))) :
      Set S)
have insert : (∃ (y : AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))),
    (AdjoinRoot.liftAlgHom (Polynomial.map (algebraMap R S') (minpoly R a)) (Algebra.ofId S' S) a sorry :
          (a : AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))) → S)
        y =
      a) ∧
  (↑s : Set S) ⊆
    Set.range.{u_1, u + 1} (ι := AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
      (⇑(AdjoinRoot.liftAlgHom (Polynomial.map (algebraMap R S') (minpoly R a)) (Algebra.ofId S' S) a sorry) :
        (a : AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))) → S)
Tactic: simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]
-- 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 : 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)
have empty : ∃ (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), (↑∅ : Set S) ⊆ (↑f.range : Set S)
Tactic: 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⟩⟩
Cleared hypotheses: 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.Finite R S
s : Finset S
empty :
  ∃ (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), (↑∅ : 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), (↑s : Set S) ⊆ (↑f.range : Set S)
have insert : ∀ (a : S) (s : Finset S) (has : a ∉ s)
  (IH :
    ∃ (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), (↑(insert a s) : Set S) ⊆ (↑f.range : Set S)
Tactic: 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⟩⟩
Cleared hypotheses: s