awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ FinitePresentation R S
have obtain : ∀ (l : (↑(↑s : Set S) : Type u_2) →₀ S)
  (hl :
    Eq (α := S)
      ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
            (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
          l :
        S)
      (1 : S)),
  FinitePresentation R S
Tactic: obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
      (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
⊢ FinitePresentation R S
have choose : ∀ (g' : (g : ↥s) → MvPolynomial (Fin n) R) (hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)),
  FinitePresentation R S
Tactic: choose g' hg' using (fun g : s ↦ hf g)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
⊢ FinitePresentation R S
have choose : ∀ (h' : (g : ↥s) → MvPolynomial (Fin n) R)
  (hh' :
    ∀ (g : ↥s),
      Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
        ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)),
  FinitePresentation R S
Tactic: choose h' hh' using (fun g : s ↦ hf (l g))
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
p : MvPolynomial (Fin n) R
hp : p ∈ I
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) p : S) (0 : S)
have hp₁ : HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, g' g * h' g) 1 ∣ p
Tactic: simp only [Finset.univ_eq_attach, I, Ideal.mem_span_singleton] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
p : MvPolynomial (Fin n) R
hp : HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, g' g * h' g) 1 ∣ p
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) p : S) (0 : S)
have obtain : ∀ (q : MvPolynomial (Fin n) R),
  Eq.{u_2 + 1} (α := S)
    ((f : (a : MvPolynomial (Fin n) R) → S)
        (HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, g' g * h' g) 1 * q) :
      S)
    (0 : S)
Tactic: obtain ⟨q, rfl⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ Eq.{u_2 + 1} (α := S)
    ((f : (a : MvPolynomial (Fin n) R) → S)
        (HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, g' g * h' g) 1 * q) :
      S)
    (0 : S)
have simp : HMul.hMul (β := S)
    (HSub.hSub (α := S) (∑ x ∈ s.attach, HMul.hMul (β := S) (↑x : S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) x : S))
      1)
    ((f : (a : MvPolynomial (Fin n) R) → S) q : S) =
  0
Tactic: simp only [map_mul, map_sub, map_sum, map_one, hg', hh']
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ HMul.hMul (β := S)
      (HSub.hSub (α := S)
        (∑ x ∈ s.attach, HMul.hMul (β := S) (↑x : S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) x : S)) 1)
      ((f : (a : MvPolynomial (Fin n) R) → S) q : S) =
    0
have rw : ∀
  (hl :
    Eq (α := S) (∑ i ∈ s.attach, HSMul.hSMul (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (↑i : S)) 1)
  (g' : (g : ↥s) → MvPolynomial (Fin n) R) (hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S))
  (h' : (g : ↥s) → MvPolynomial (Fin n) R)
  (hh' :
    ∀ (g : ↥s),
      Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
        ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S))
  (q : MvPolynomial (Fin n) R),
  HMul.hMul (β := S)
      (HSub.hSub (α := S)
        (∑ x ∈ s.attach, HMul.hMul (β := S) (↑x : S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) x : S)) 1)
      ((f : (a : MvPolynomial (Fin n) R) → S) q : S) =
    0
Tactic: rw [Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)] at hl
Cleared hypotheses: hl, g', hg', h', hh', I, A, q
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
rw :
  ∀
    (hl :
      Eq (α := S) (∑ i ∈ s.attach, HSMul.hSMul (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (↑i : S)) 1)
    (g' : (g : ↥s) → MvPolynomial (Fin n) R)
    (hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S))
    (h' : (g : ↥s) → MvPolynomial (Fin n) R)
    (hh' :
      ∀ (g : ↥s),
        Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
          ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S))
    (q : MvPolynomial (Fin n) R),
    HMul.hMul (β := S)
        (HSub.hSub (α := S)
          (∑ x ∈ s.attach, HMul.hMul (β := S) (↑x : S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) x : S)) 1)
        ((f : (a : MvPolynomial (Fin n) R) → S) q : S) =
      0
⊢ HMul.hMul (β := S)
      (HSub.hSub (α := S)
        (∑ x ∈ s.attach, HMul.hMul (β := S) (↑x : S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) x : S)) 1)
      ((f : (a : MvPolynomial (Fin n) R) → S) q : S) =
    0
have rw₁ : Membership.mem (γ := Submodule S ((↑(↑s : Set S) : Type u_2) →₀ S))
  (Finsupp.supported S S (↑s.attach : Set (↑(↑s : Set S) : Type u_2))) l
Tactic: rw [Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)] at hl
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl : Eq (α := S) (∑ i ∈ s.attach, HSMul.hSMul (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (↑i : S)) 1
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ HMul.hMul (β := S)
      (HSub.hSub (α := S)
        (∑ x ∈ s.attach, HMul.hMul (β := S) (↑x : S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) x : S)) 1)
      ((f : (a : MvPolynomial (Fin n) R) → S) q : S) =
    0
have rw : HMul.hMul (β := S)
    (HSub.hSub (α := S) (∑ x ∈ s.attach, HMul.hMul (β := S) (↑x : S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) x : S))
      (∑ i ∈ s.attach, HSMul.hSMul (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (↑i : S)))
    ((f : (a : MvPolynomial (Fin n) R) → S) q : S) =
  0
Tactic: rw [← hl]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
⊢ FinitePresentation R S
have hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
Tactic: have hfI : ∀ a ∈ I, f a = 0 := by
    intro p hp
    simp only [Finset.univ_eq_attach, I, Ideal.mem_span_singleton] at hp
    obtain ⟨q, rfl⟩ := hp
    simp only [map_mul, map_sub, map_sum, map_one, hg', hh']
    rw [Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)] at hl
    · rw [← hl]
      simp only [Finset.coe_sort_coe, smul_eq_mul, mul_comm, sub_self, zero_mul]
    · rintro a -
      simp
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
⊢ FinitePresentation R S
have hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
Tactic: have hf' : Function.Surjective f' :=
    Ideal.Quotient.lift_surjective_of_surjective I hfI hf
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
⊢ Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
have rw : Membership.mem (γ := Ideal A) (Ideal.span (↑t : Set A)) 1
Tactic: rw [Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
⊢ Eq (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1
have h₂ : HSub.hSub (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1 =
  0
Tactic: apply eq_of_sub_eq_zero