awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Lattice
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 ι)
intro : Module.Finite.{u_2, u_3} R ↥(Finset.sup Finset.univ fun (i : PLift ι) ↦ S i.down)
⊢ Module.Finite.{u_2, u_3} R ↥(⨆ (i : ι), S i)

Tactic:
rw [← iSup_plift_down, ← Finset.sup_univ_eq_iSup]

Premises used: iSup_plift_down, Finset.sup_univ_eq_iSup
-- Module: Mathlib.RingTheory.Finiteness.Lattice
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 ↥(Finset.sup Finset.univ fun (i : PLift ι) ↦ S i.down)

Tactic:
Submodule.finite_finset_sup _ _

Premises used: Set.Mem, Submodule.finite_finset_sup
-- Module: Mathlib.RingTheory.Finiteness.Lattice
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 ↥(Finset.sup Finset.univ fun (i : PLift ι) ↦ S i.down)

Tactic:
exact Submodule.finite_finset_sup _ _

Premises used: Submodule.finite_finset_sup
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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
⊢ Submodule.FG.{u, u_1} (R := R) (M := S) ⊤

Tactic:
Module.finite_def.mp inferInstance

Premises used: inferInstance, Module.finite_def, Iff.mp
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)

Tactic:
obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance

Premises used: inferInstance, Submodule.FG, Module.finite_def, Iff.mp, Top.top
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)
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)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)
⊢ Submodule.span R (↑s : Set S) ≤ f.toLinearMap.range

Tactic:
have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)
rwa₂ rwa₃ rwa₄ 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)
⊢ 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

Premises used: LinearMap.range_eq_top, top_le_iff
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)

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
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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_1 : CommRing S'
w_2 : Algebra R S'
w_3 : Module.Finite R S'
w_4 : Free R S'
w_5 : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : (↑s : Set S) ⊆ (↑f.range : Set S)
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
w : Type u
w₁ : CommRing S'
w₂ : Algebra R S'
w₃ : Module.Finite R S'
w₄ : Free R S'
w₅ : Algebra.FinitePresentation R S'
w₆ : S' →ₐ[R] S
h : 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)

Tactic:
use S', ‹_›, ‹_›, ‹_›, ‹_›, ‹_›, f
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)) ⊤
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)
⊢ ∃ (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:
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
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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
⊢ (↑∅ : Set S) ⊆ (↑(AlgHom.range (Algebra.ofId R S)) : Set S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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), (↑∅ : Set S) ⊆ (↑f.range : Set S)

Tactic:
exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)
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.insert a 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.insert a s) : Set S) ⊆ (↑f.range : Set S)

Tactic:
obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)
⊢ IsIntegral R a

Tactic:
have ha := Algebra.IsIntegral.isIntegral (R := R) a
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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
⊢ Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))

Tactic:
have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)))
⊢ Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))

Tactic:
have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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
⊢ Polynomial.eval₂ (↑(Algebra.ofId S' S) : S' →+* S) a (Polynomial.map (algebraMap R S') (minpoly R a)) = 0

Tactic:
simp [← Polynomial.aeval_def]

Premises used: Polynomial.aeval_def
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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 :
  (↑(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 ⋯))) :
      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.insert a s) : Set S) ⊆ (↑f.range : 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, ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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 :
  (∃ (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 ⋯ :
            (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 ⋯) :
          (a : AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))) → S)
⊢ (↑(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 ⋯))) :
      Set S)

Tactic:
simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]

Premises used: Set.mem_range, AlgHom.coe_range, Set.insert_subset_iff, AlgHom.coe_restrictScalars', Finset.coe_insert
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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
⊢ (AdjoinRoot.liftAlgHom (Polynomial.map (algebraMap R S') (minpoly R a)) (Algebra.ofId S' S) a ⋯ :
        (a : AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))) → S)
      (AdjoinRoot.root (Polynomial.map (algebraMap R S') (minpoly R a))) =
    a

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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
y : S
h : y ∈ (↑f.range : Set S)
x : S'
hx : (f.toRingHom : (a : S') → S) x = y
⊢ (AdjoinRoot.liftAlgHom (Polynomial.map (algebraMap R S') (minpoly R a)) (Algebra.ofId S' S) a ⋯ :
        (a : AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))) → S)
      ((AdjoinRoot.of (Polynomial.map (algebraMap R S') (minpoly R a)) :
            (a_1 : S') → AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
          x :
        AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))) =
    y

Tactic:
simpa
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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
⊢ (∃ (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 ⋯ :
            (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 ⋯) :
          (a : AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a))) → S)

Tactic:
exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)
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.insert a 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)

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⟩⟩

Premises used: Set.mem_range, AlgHom.coe_range, Insert.insert, Set.insert_subset_iff, AlgHom.coe_restrictScalars', Finset.coe_insert
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
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)
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)
⊢ ∃ (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⟩⟩

Premises used: Set.mem_range, AlgHom.coe_range, inferInstance, Insert.insert, Submodule.FG, Set.insert_subset_iff, AlgHom.coe_restrictScalars', Module.finite_def, Iff.mp, Top.top, Finset.coe_insert