awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin n) R) S)
    (hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S))
    (hg' : Ideal.FG (ker g')),
    let this := (g'.comp MvPolynomial.C).toAlgebra;
    Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
g' : RingHom.{u, v} (MvPolynomial (Fin (n + 1)) R) S
hg :
  Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin (n + 1)) R) (β := S) (⇑g' : (a : MvPolynomial (Fin (n + 1)) R) → S)
hg' : Ideal.FG (ker g')
this_1 : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  AlgEquiv.trans (MvPolynomial.renameEquiv R (finSuccEquiv n)) (MvPolynomial.optionEquivRight R (Fin n))
he :
  Ideal.FG
    (ker (F := RingHom.{u, v} (MvPolynomial (Fin n) R[X]) S)
      (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)))
this :
  Q R[X] S
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C)
⊢ g'.comp MvPolynomial.C =
    g'.comp
      (RingHom.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
        (RingHom.comp MvPolynomial.C C))
have h : ∀ (r : R) (m : Fin (n + 1) →₀ ℕ),
  Eq.{u + 1} (α := R) (MvPolynomial.coeff m ((MvPolynomial.C : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
    (MvPolynomial.coeff m
      ((RingHom.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
            (RingHom.comp MvPolynomial.C C) :
          (a : R) → MvPolynomial (Fin (n + 1)) R)
        r))
Tactic: congr 1 with r
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
n : ℕ
g' : RingHom.{u, v} (MvPolynomial (Fin n) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Q R S (g'.comp MvPolynomial.C)
have zero : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S)
  (hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S))
  (hg' : Ideal.FG (ker g')), Q R S (g'.comp MvPolynomial.C)
Tactic: induction n generalizing R S with
  | zero =>
    refine fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_
    rw [← comap_ker]
    convert! hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom using 1
    simp only [RingEquiv.toRingHom_eq_coe]
    exact Ideal.comap_symm (MvPolynomial.isEmptyRingEquiv R (Fin 0))
  | succ n IH =>
    let e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
      (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
    have he : (ker (g'.comp <| RingHomClass.toRingHom e.symm)).FG := by
      rw [← RingHom.comap_ker]
      convert! hg'.map e.toAlgHom.toRingHom using 1
      exact Ideal.comap_symm e.toRingEquiv
    have := IH (R := R[X]) (S := S) (g'.comp e.symm) (hg.comp e.symm.surjective) he
    convert! comp _ _ _ _ _ (polynomial _) this using 1
    rw [comp_assoc, comp_assoc]
    congr 1 with r
    simp [e]
Cleared hypotheses: R, S, inst, inst_1, n, g', hg, hg', this
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
n : ℕ
g' : RingHom.{u, v} (MvPolynomial (Fin n) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
zero :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S)
    (hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S))
    (hg' : Ideal.FG (ker g')), Q R S (g'.comp MvPolynomial.C)
⊢ Q R S (g'.comp MvPolynomial.C)
have succ : ∀ (n : ℕ)
  (IH :
    ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S]
      (g' : RingHom.{u, v} (MvPolynomial (Fin n) R) S)
      (hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S))
      (hg' : Ideal.FG (ker g')),
      let this := (g'.comp MvPolynomial.C).toAlgebra;
      Q R S (g'.comp MvPolynomial.C))
  {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S]
  (g' : RingHom.{u, v} (MvPolynomial (Fin (n + 1)) R) S)
  (hg :
    Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin (n + 1)) R) (β := S)
      (⇑g' : (a : MvPolynomial (Fin (n + 1)) R) → S))
  (hg' : Ideal.FG (ker g')), Q R S (g'.comp MvPolynomial.C)
Tactic: induction n generalizing R S with
  | zero =>
    refine fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_
    rw [← comap_ker]
    convert! hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom using 1
    simp only [RingEquiv.toRingHom_eq_coe]
    exact Ideal.comap_symm (MvPolynomial.isEmptyRingEquiv R (Fin 0))
  | succ n IH =>
    let e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
      (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
    have he : (ker (g'.comp <| RingHomClass.toRingHom e.symm)).FG := by
      rw [← RingHom.comap_ker]
      convert! hg'.map e.toAlgHom.toRingHom using 1
      exact Ideal.comap_symm e.toRingEquiv
    have := IH (R := R[X]) (S := S) (g'.comp e.symm) (hg.comp e.symm.surjective) he
    convert! comp _ _ _ _ _ (polynomial _) this using 1
    rw [comp_assoc, comp_assoc]
    congr 1 with r
    simp [e]
Cleared hypotheses: R, S, inst, inst_1, n, g', hg, hg', this
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)
⊢ Function.Surjective (α := B ⊗[R] MvPolynomial σ R) (β := B ⊗[R] A)
    (⇑(TensorProduct.map (AlgHom.id B B) f : B ⊗[R] MvPolynomial σ R →ₐ[B] B ⊗[R] A) :
      (a : B ⊗[R] MvPolynomial σ R) → B ⊗[R] A)
have change : Function.Surjective (α := B ⊗[R] MvPolynomial σ R) (β := B ⊗[R] A)
  (⇑(TensorProduct.map (AlgHom.id R B) f : B ⊗[R] MvPolynomial σ R →ₐ[R] B ⊗[R] A) :
    (a : B ⊗[R] MvPolynomial σ R) → B ⊗[R] A)
Tactic: change Function.Surjective (TensorProduct.map (AlgHom.id R B) f)
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)
⊢ Function.Surjective (α := B ⊗[R] MvPolynomial σ R) (β := B ⊗[R] A)
    (⇑(TensorProduct.map (AlgHom.id R B) f : B ⊗[R] MvPolynomial σ R →ₐ[R] B ⊗[R] A) :
      (a : B ⊗[R] MvPolynomial σ R) → B ⊗[R] A)
have hf₁ : Function.Surjective (α := B) (β := B) (⇑(AlgHom.id R B) : (a : B) → B)
Tactic: apply TensorProduct.map_surjective
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
hfa : FiniteType R A
⊢ FiniteType B (B ⊗[R] A)
have rw : ∀
  (hfa :
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A),
      Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A)
        (⇑f : (a : MvPolynomial (Fin n) R) → A)),
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A),
    Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑f : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
Tactic: rw [iff_quotient_mvPolynomial''] at *
Cleared hypotheses: hfa
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
hfa :
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A),
    Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A),
    Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑f : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
have obtain : ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
  (hf :
    Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A)
      (⇑f : (a : MvPolynomial (Fin n) R) → A)),
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A),
    Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑f : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
Tactic: obtain ⟨n, f, hf⟩ := hfa
Cleared hypotheses: hfa
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (hypothesis)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A),
    Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑f : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
have this : Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
  (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
Tactic: have : Function.Surjective g := baseChangeAux_surj B hf
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
this :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A),
    Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑f : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
have h : Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A)
  (⇑(g.comp
        (↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
          MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)) :
    (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
Tactic: use n, AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
⊢ FinitePresentation B (B ⊗[R] A)
have obtain : ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
  (hsurj :
    Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A))
  (hfg : Ideal.FG (RingHom.ker f.toRingHom)), FinitePresentation B (B ⊗[R] A)
Tactic: obtain ⟨n, f, hsurj, hfg⟩ := ‹FinitePresentation R A›
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (hypothesis)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
⊢ FinitePresentation B (B ⊗[R] A)
have hgsurj : Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
  (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
Tactic: have hgsurj : Function.Surjective g := Algebra.FiniteType.baseChangeAux_surj B hsurj
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (hypothesis)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
⊢ FinitePresentation B (B ⊗[R] A)
have hker_eq : Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
  (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
    (RingHom.ker f))
Tactic: have hker_eq : RingHom.ker g = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker f) :=
    Algebra.TensorProduct.lTensor_ker f hsurj
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
hker_eq :
  Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
    (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
      (RingHom.ker f))
⊢ Ideal.FG (RingHom.ker g)
have rw : Ideal.FG (R := B ⊗[R] MvPolynomial (Fin n) R)
  (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
    (RingHom.ker f))
Tactic: rw [hker_eq]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (hypothesis)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
hker_eq :
  Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
    (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
      (RingHom.ker f))
⊢ FinitePresentation B (B ⊗[R] A)
have hfgg : Ideal.FG (RingHom.ker g)
Tactic: have hfgg : Ideal.FG (RingHom.ker g) := by
    rw [hker_eq]
    exact Ideal.FG.map hfg _
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
hker_eq :
  Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
    (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
      (RingHom.ker f))
hfgg : Ideal.FG (RingHom.ker g)
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A :=
  g.comp
    (↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
      MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
⊢ FinitePresentation B (B ⊗[R] A)
have refine_1 : Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑g' : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
Tactic: refine ⟨n, g', ?_, Ideal.fg_ker_comp _ _ ?_ hfgg ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
hker_eq :
  Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
    (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
      (RingHom.ker f))
hfgg : Ideal.FG (RingHom.ker g)
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A :=
  g.comp
    (↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
      MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
refine_1 :
  Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑g' : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
⊢ FinitePresentation B (B ⊗[R] A)
have refine_2 : Ideal.FG
  (RingHom.ker (F := MvPolynomial (Fin n) B →+* B ⊗[R] MvPolynomial (Fin n) R)
    (↑(↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
          MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R) :
      MvPolynomial (Fin n) B →+* B ⊗[R] MvPolynomial (Fin n) R))
Tactic: refine ⟨n, g', ?_, Ideal.fg_ker_comp _ _ ?_ hfgg ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
hker_eq :
  Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
    (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
      (RingHom.ker f))
hfgg : Ideal.FG (RingHom.ker g)
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A :=
  g.comp
    (↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
      MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
refine_1 :
  Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑g' : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)
refine_2 :
  Ideal.FG
    (RingHom.ker (F := MvPolynomial (Fin n) B →+* B ⊗[R] MvPolynomial (Fin n) R)
      (↑(↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
            MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R) :
        MvPolynomial (Fin n) B →+* B ⊗[R] MvPolynomial (Fin n) R))
⊢ FinitePresentation B (B ⊗[R] A)
have refine_3 : Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] MvPolynomial (Fin n) R)
  (⇑(↑(↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
            MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R) :
        MvPolynomial (Fin n) B →+* B ⊗[R] MvPolynomial (Fin n) R) :
    (a : MvPolynomial (Fin n) B) → B ⊗[R] MvPolynomial (Fin n) R)
Tactic: refine ⟨n, g', ?_, Ideal.fg_ker_comp _ _ ?_ hfgg ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
hker_eq :
  Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
    (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
      (RingHom.ker f))
hfgg : Ideal.FG (RingHom.ker g)
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A :=
  g.comp
    (↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
      MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
⊢ Ideal.FG
    (RingHom.ker (F := MvPolynomial (Fin n) B →+* B ⊗[R] MvPolynomial (Fin n) R)
      (↑(↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
            MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R) :
        MvPolynomial (Fin n) B →+* B ⊗[R] MvPolynomial (Fin n) R))
have refine_2 : Ideal.FG
  (RingHom.ker (F := MvPolynomial (Fin n) B ≃ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
    (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))
Tactic: change Ideal.FG (RingHom.ker (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))