awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
leI :
  LE.le (α := Ideal (MvPolynomial (Fin n) A))
    (Ideal.span
      ((⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
          (↑s : Set (MvPolynomial (Fin n) R)) ∪
        Set.range g))
    (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
      (MvPolynomial.aeval
        (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
          MvPolynomial.X)))
⊢ Ideal.span s₀ = I
have refine_2 : LE.le (α := Ideal (MvPolynomial (Fin n) A))
  (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X)))
  (Ideal.span
    ((⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
        (↑s : Set (MvPolynomial (Fin n) R)) ∪
      Set.range g))
Tactic: apply leI.antisymm
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have obtain : ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
  (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
  (s : Finset (MvPolynomial (Fin m) R))
  (hs :
    Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
      (RingHom.ker f'.toRingHom)),
  Ideal.FG (RingHom.ker f.toRingHom)
Tactic: obtain ⟨m, f', hf', s, hs⟩ := FinitePresentation.out (R := R) (A := A)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have this : ∀ (i : Fin n),
  ∃ (a : MvPolynomial (Fin m) R),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) a : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
Tactic: have := fun i : Fin n => hf' (f <| X i)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
this :
  ∀ (i : Fin n),
    ∃ (a : MvPolynomial (Fin m) R),
      Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) a : A)
        ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have choose : ∀ (g : (i : Fin n) → MvPolynomial (Fin m) R)
  (hg :
    ∀ (i : Fin n),
      Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
        ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)),
  Ideal.FG (RingHom.ker f.toRingHom)
Tactic: choose g hg using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have this : ∀ (i : Fin m),
  ∃ (a : MvPolynomial (Fin n) R),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) a : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
Tactic: have := fun i : Fin m => hf (f' <| X i)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
this :
  ∀ (i : Fin m),
    ∃ (a : MvPolynomial (Fin n) R),
      Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) a : A)
        ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have choose : ∀ (h : (i : Fin m) → MvPolynomial (Fin n) R)
  (hh :
    ∀ (i : Fin m),
      Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
        ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
  Ideal.FG (RingHom.ker f.toRingHom)
Tactic: choose h hh using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have refine : Eq (α := Ideal (MvPolynomial (Fin n) R))
  (Ideal.span
    (↑(Finset.image g' Finset.univ ∪ Finset.image (⇑aeval_h : (a : RXm) → RXn) s) : Set (MvPolynomial (Fin n) R)))
  (RingHom.ker f.toRingHom)
Tactic: refine ⟨Finset.univ.image g' ∪ s.image aeval_h, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.span
      (↑(Finset.image g' Finset.univ ∪ Finset.image (⇑aeval_h : (a : RXm) → RXn) s) : Set (MvPolynomial (Fin n) R)))
    (RingHom.ker f.toRingHom)
have simp : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)))
  (RingHom.ker f.toRingHom)
Tactic: simp only [Finset.coe_image, Finset.coe_union, Finset.coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
x : RXm
⊢ Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
have rw : Eq.{w₂ + 1} (α := A)
  ((eval₂Hom
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin n) R →+* A)
            (algebraMap R (MvPolynomial (Fin n) R)))
          fun (i : Fin m) ↦ ((↑f : MvPolynomial (Fin n) R →+* A) : (a : MvPolynomial (Fin n) R) → A) (h i) :
        (a : MvPolynomial (Fin m) R) → A)
      x :
    A)
  ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
Tactic: rw [← f.coe_toRingHom, map_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
x : RXm
⊢ Eq.{w₂ + 1} (α := A)
    ((eval₂Hom
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin n) R →+* A)
              (algebraMap R (MvPolynomial (Fin n) R)))
            fun (i : Fin m) ↦ ((↑f : MvPolynomial (Fin n) R →+* A) : (a : MvPolynomial (Fin n) R) → A) (h i) :
          (a : MvPolynomial (Fin m) R) → A)
        x :
      A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
have simp_rw : Eq.{w₂ + 1} (α := A)
  ((eval₂Hom
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin n) R →+* A)
            (algebraMap R (MvPolynomial (Fin n) R)))
          fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
        (a : MvPolynomial (Fin m) R) → A)
      x :
    A)
  ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
Tactic: simp_rw [AlgHom.coe_toRingHom, hh]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
x : RXm
⊢ Eq.{w₂ + 1} (α := A)
    ((eval₂Hom
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin n) R →+* A)
              (algebraMap R (MvPolynomial (Fin n) R)))
            fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
          (a : MvPolynomial (Fin m) R) → A)
        x :
      A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
have rw : Eq.{w₂ + 1} (α := A)
  ((eval₂Hom (algebraMap R A) fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
        (a : MvPolynomial (Fin m) R) → A)
      x :
    A)
  ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
Tactic: rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
        -- Porting note: added line below
        ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),
        ← aeval_unique]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
x : RXm
rw :
  Eq.{w₂ + 1} (α := A)
    ((eval₂Hom (algebraMap R A) fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
          (a : MvPolynomial (Fin m) R) → A)
        x :
      A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
⊢ Eq.{w₂ + 1} (α := A)
    ((eval₂Hom
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin n) R →+* A)
              (algebraMap R (MvPolynomial (Fin n) R)))
            fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
          (a : MvPolynomial (Fin m) R) → A)
        x :
      A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
have rw₁ : Eq.{w₂ + 1} (α := A)
  ((MvPolynomial.aeval fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
        (a : MvPolynomial (Fin m) R) → A)
      x :
    A)
  ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
Tactic: rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
        -- Porting note: added line below
        ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),
        ← aeval_unique]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
x : RXm
rw :
  Eq.{w₂ + 1} (α := A)
    ((eval₂Hom (algebraMap R A) fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
          (a : MvPolynomial (Fin m) R) → A)
        x :
      A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
rw₁ :
  Eq.{w₂ + 1} (α := A)
    ((MvPolynomial.aeval fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
          (a : MvPolynomial (Fin m) R) → A)
        x :
      A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
⊢ Eq.{w₂ + 1} (α := A)
    ((eval₂Hom
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin n) R →+* A)
              (algebraMap R (MvPolynomial (Fin n) R)))
            fun (i : Fin m) ↦ (f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) :
          (a : MvPolynomial (Fin m) R) → A)
        x :
      A)
    ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
have rw₂ : Eq.{w₂ + 1} (α := A)
  ((MvPolynomial.aeval fun (i : Fin m) ↦
          Function.comp.{1, w₁ + 1, w₂ + 1} (β := MvPolynomial (Fin m) R) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
            MvPolynomial.X i :
        (a : MvPolynomial (Fin m) R) → A)
      x :
    A)
  ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
Tactic: rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
        -- Porting note: added line below
        ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),
        ← aeval_unique]