awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteStability
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 (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)

Tactic:
hf
-- Module: Mathlib.RingTheory.FiniteStability
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 (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)

Tactic:
exact hf
-- Module: Mathlib.RingTheory.FiniteStability
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
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)
⊢ FiniteType B (B ⊗[R] A)

Tactic:
rw [iff_quotient_mvPolynomial''] at *

Premises used: Algebra.FiniteType.iff_quotient_mvPolynomial''
-- Module: Mathlib.RingTheory.FiniteStability
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)
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)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.FiniteStability
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
⊢ 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
-- Module: Mathlib.RingTheory.FiniteStability
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)
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)
⊢ ∃ (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:
use n, AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, MvPolynomial.algebraTensorAlgEquiv, AlgHom.comp
-- Module: Mathlib.RingTheory.FiniteStability
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)
⊢ 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:
simpa
-- Module: Mathlib.RingTheory.FiniteStability
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
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)
⊢ FinitePresentation B (B ⊗[R] A)

Tactic:
obtain ⟨n, f, hsurj, hfg⟩ := ‹FinitePresentation R A›

Premises used: Algebra.FinitePresentation
-- Module: Mathlib.RingTheory.FiniteStability
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
⊢ 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
-- Module: Mathlib.RingTheory.FiniteStability
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)
⊢ 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
-- Module: Mathlib.RingTheory.FiniteStability
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))
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))
⊢ Ideal.FG (RingHom.ker g)

Tactic:
rw [hker_eq]
-- Module: Mathlib.RingTheory.FiniteStability
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 (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:
Ideal.FG.map hfg _

Premises used: Ideal.FG.map, Ideal.map, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.FiniteStability
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 (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:
exact Ideal.FG.map hfg _

Premises used: Ideal.FG.map
-- Module: Mathlib.RingTheory.FiniteStability
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)

Tactic:
have hfgg : Ideal.FG (RingHom.ker g) := by
    rw [hker_eq]
    exact Ideal.FG.map hfg _
-- Module: Mathlib.RingTheory.FiniteStability
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)

Tactic:
⟨n, g', ?_, Ideal.fg_ker_comp _ _ ?_ hfgg ?_⟩

Premises used: Algebra.FinitePresentation.mk, Ideal.fg_ker_comp, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.FiniteStability
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))
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)
⊢ FinitePresentation B (B ⊗[R] A)

Tactic:
refine ⟨n, g', ?_, Ideal.fg_ker_comp _ _ ?_ hfgg ?_⟩
-- Module: Mathlib.RingTheory.FiniteStability
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)
⊢ Function.Surjective (α := MvPolynomial (Fin n) B) (β := B ⊗[R] A) (⇑g' : (a : MvPolynomial (Fin n) B) → B ⊗[R] A)

Tactic:
simp_all [g, g']
-- Module: Mathlib.RingTheory.FiniteStability
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_2 :
  Ideal.FG
    (RingHom.ker (F := MvPolynomial (Fin n) B ≃ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
      (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))
⊢ 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:
change Ideal.FG (RingHom.ker (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))

Premises used: AlgEquiv.symm, Ideal.FG, MvPolynomial.algebraTensorAlgEquiv, RingHom.ker
-- Module: Mathlib.RingTheory.FiniteStability
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_2 : Ideal.FG.{w₃} (R := MvPolynomial (Fin n) B) ⊥
⊢ Ideal.FG
    (RingHom.ker (F := MvPolynomial (Fin n) B ≃ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
      (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))

Tactic:
simp only [RingHom.ker_equiv]

Premises used: RingHom.ker_equiv
-- Module: Mathlib.RingTheory.FiniteStability
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.{w₃} (R := MvPolynomial (Fin n) B) ⊥

Tactic:
Submodule.fg_bot

Premises used: Submodule.FG, Ideal.FG, Submodule.fg_bot
-- Module: Mathlib.RingTheory.FiniteStability
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.{w₃} (R := MvPolynomial (Fin n) B) ⊥

Tactic:
exact Submodule.fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.FiniteStability
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)
⊢ 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:
simpa using EquivLike.surjective _

Premises used: EquivLike.surjective
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R_1 : Type uR
S : Type uS
A_1 : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : Semiring A
inst_7 : Algebra R A
hRA : Module.Finite R A
⊢ Algebra.FiniteType R A

Tactic:
⟨Subalgebra.fg_of_submodule_fg hRA.1⟩

Premises used: Module.Finite.fg_top, Subalgebra.fg_of_submodule_fg, Algebra.FiniteType.mk