awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.comap (Q.aux P)
      (RingHom.ker (F := MvPolynomial ι' S →ₐ[R] T) (aevalTower (IsScalarTower.toAlgHom R S T) Q.val)))
have change : Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
  (Ideal.span
    (Set.range (ι := σ' ⊕ σ)
      (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
        (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
  (Ideal.comap (Q.aux P) (RingHom.ker (F := MvPolynomial ι' S →ₐ[S] T) (aeval Q.val)))
Tactic: change _ = Ideal.comap _ (RingHom.ker (aeval Q.val))
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.comap (Q.aux P) (RingHom.ker (F := MvPolynomial ι' S →ₐ[S] T) (aeval Q.val)))
have rw : Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
  (Ideal.span
    (Set.range (ι := σ' ⊕ σ)
      (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
        (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
  (Ideal.span (Set.range (Q.compRelationAux P)) ⊔ RingHom.ker (Q.aux P))
Tactic: rw [← Q.ker_eq_ker_aeval_val, ← Q.span_range_relation_eq_ker, ← Q.aux_image_relation P,
    ← Ideal.map_span, Ideal.comap_map_of_surjective' _ (Q.aux_surjective P)]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔ RingHom.ker (Q.aux P))
have rw : Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
  (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
    Ideal.span
      (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp)))
  (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
    Ideal.span ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation))
Tactic: rw [Set.Sum.elim_range, Ideal.span_union, Q.aux_ker, ← P.ker_eq_ker_aeval_val,
    ← P.span_range_relation_eq_ker, Ideal.map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
      Ideal.span
        (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp)))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
      Ideal.span ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation))
have e_a : Eq (α := Set (MvPolynomial (ι' ⊕ ι) R))
  (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))
  ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
⊢ Eq (α := Set (MvPolynomial (ι' ⊕ ι) R))
    (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))
    ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation)
have e_a : ∀ (x : MvPolynomial (ι' ⊕ ι) R),
  Membership.mem (γ := Set (MvPolynomial (ι' ⊕ ι) R))
      (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp)) x ↔
    Membership.mem (γ := Set (MvPolynomial (ι' ⊕ ι) R))
      ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ relation (comp (localizationAway T g) P) (Sum.inl r) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) -
      1
have simp : (Finsupp.sum
    (HAdd.hAdd (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
      ((monomial (Finsupp.single () 1) : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S)
      ((C : (a : S) → MvPolynomial Unit S) (-1) : MvPolynomial Unit S))
    fun (x : Unit →₀ ℕ) (j : S) ↦
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ j) : MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((monomial (Finsupp.mapDomain Sum.inl x) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
        MvPolynomial.{w, u} (Unit ⊕ ι) R)) =
  HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) : MvPolynomial.{w, u} (Unit ⊕ ι) R)
      (X (Sum.inl ())) +
    (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)
Tactic: simp only [Presentation.comp, Sum.elim_inl, Presentation.compRelationAux,
    Presentation.localizationAway_relation, sub_eq_add_neg, C_mul_X_eq_monomial,
    ← map_one C, ← map_neg C]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ (Finsupp.sum
      (HAdd.hAdd (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
        ((monomial (Finsupp.single () 1) : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S)
        ((C : (a : S) → MvPolynomial Unit S) (-1) : MvPolynomial Unit S))
      fun (x : Unit →₀ ℕ) (j : S) ↦
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ j) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl x) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)
have refine_1 : Ne (α := Unit →₀ ℕ) (Finsupp.single () 1) 0
Tactic: refine (Finsupp.sum_single_add_single (Finsupp.single () 1) 0 g (-1 : S) _ ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
refine_1 : Ne (α := Unit →₀ ℕ) (Finsupp.single () 1) 0
⊢ (Finsupp.sum
      (HAdd.hAdd (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
        ((monomial (Finsupp.single () 1) : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S)
        ((C : (a : S) → MvPolynomial Unit S) (-1) : MvPolynomial Unit S))
      fun (x : Unit →₀ ℕ) (j : S) ↦
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ j) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl x) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)
have refine_2 : ∀ (f : Unit →₀ ℕ),
  HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ 0) : MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((monomial (Finsupp.mapDomain Sum.inl f) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
        MvPolynomial.{w, u} (Unit ⊕ ι) R) =
    0
Tactic: refine (Finsupp.sum_single_add_single (Finsupp.single () 1) 0 g (-1 : S) _ ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
refine_1 : Ne (α := Unit →₀ ℕ) (Finsupp.single () 1) 0
refine_2 :
  ∀ (f : Unit →₀ ℕ),
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ 0) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl f) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R) =
      0
⊢ (Finsupp.sum
      (HAdd.hAdd (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
        ((monomial (Finsupp.single () 1) : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S)
        ((C : (a : S) → MvPolynomial Unit S) (-1) : MvPolynomial Unit S))
      fun (x : Unit →₀ ℕ) (j : S) ↦
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ j) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl x) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)
have refine_3 : HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) : MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((monomial (Finsupp.mapDomain Sum.inl (Finsupp.single () 1)) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
        MvPolynomial.{w, u} (Unit ⊕ ι) R) +
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ (-1)) :
        MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((monomial (Finsupp.mapDomain Sum.inl 0) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
        MvPolynomial.{w, u} (Unit ⊕ ι) R) =
  HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) : MvPolynomial.{w, u} (Unit ⊕ ι) R)
      (X (Sum.inl ())) +
    (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)
Tactic: refine (Finsupp.sum_single_add_single (Finsupp.single () 1) 0 g (-1 : S) _ ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Ideal.span
      (Set.range (ι := σ')
        ((⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R) ∘
          P.relation ∘ (⇑f : (a : σ') → σ))) =
    (P.reindex e).ker
have rw : Eq (α := Ideal (P.reindex e).Ring)
  (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
    (Ideal.span (Set.range P.relation)))
  (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
    (Ideal.span (Set.range P.relation)))
Tactic: rw [Generators.ker_eq_ker_aeval_val, Generators.reindex_val, ← aeval_comp_rename,
      ← AlgHom.comap_ker, ← P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker,
      Set.range_comp, Set.range_comp, Equiv.range_eq_univ, Set.image_univ,
      ← Ideal.map_span (rename ⇑e.symm)]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (hypothesis)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Eq (α := Ideal (P.reindex e).Ring)
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.span (Set.range P.relation)))
    (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
      (Ideal.span (Set.range P.relation)))
have hf : Function.Bijective (α := MvPolynomial ι R) (β := MvPolynomial ι' R)
  (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)
Tactic: have hf : Function.Bijective (MvPolynomial.rename e.symm) := (renameEquiv R e.symm).bijective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf :
  Function.Bijective (α := MvPolynomial ι R) (β := MvPolynomial ι' R)
    (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)
⊢ Eq (α := Ideal (P.reindex e).Ring)
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.span (Set.range P.relation)))
    (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
      (Ideal.span (Set.range P.relation)))
have a : Eq (α := Ideal (MvPolynomial ι R))
  (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.span (Set.range P.relation))))
  (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
    (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
      (Ideal.span (Set.range P.relation))))
Tactic: apply Ideal.comap_injective_of_surjective _ hf.2
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf :
  Function.Bijective (α := MvPolynomial ι R) (β := MvPolynomial ι' R)
    (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)
⊢ Eq (α := Ideal (MvPolynomial ι R))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
        (Ideal.span (Set.range P.relation))))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
        (Ideal.span (Set.range P.relation))))
have a : Eq (α := Ideal (MvPolynomial ι R))
  (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.span (Set.range P.relation))))
  (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι R) (rename _root_.id) (Ideal.span (Set.range P.relation)))
Tactic: simp_rw [Ideal.comap_comapₐ, rename_comp_rename, Equiv.self_comp_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_1
P : Generators R S α
inst_4 : Finite α
⊢ P.ker.FG
have rw : Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))
Tactic: rw [Generators.ker_eq_ker_aeval_val]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
⊢ P.coeffs ⊆ Set.range (ι := P.Core) (⇑(algebraMap P.Core R) : (a : P.Core) → R)
have refine : (↑P.core : Set R) ⊆ Set.range (ι := P.Core) (⇑(algebraMap P.Core R) : (a : P.Core) → R)
Tactic: refine subset_trans P.coeffs_subset_core ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
R₁ : Type u_6
inst_8 : CommRing R₁
inst_9 : Algebra R₀ R₁
inst_10 : Algebra R₁ R
inst_11 : IsScalarTower R₀ R₁ R
inst_12 : Algebra R₁ S
inst_13 : IsScalarTower R₁ R S
⊢ P.HasCoeffs R₁
have refine : Subset.{u_1} (α := Set R) (Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R))
  (Set.range.{u_1, u_6 + 1} (ι := R₁) (⇑(algebraMap R₁ R) : (a : R₁) → R))
Tactic: refine ⟨subset_trans (P.coeffs_subset_range R₀) ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
x : σ
⊢ Membership.mem (γ := Set (MvPolynomial ι R))
    (Set.range (ι := MvPolynomial ι R₀)
      (⇑(MvPolynomial.map (algebraMap R₀ R)) : (a : MvPolynomial ι R₀) → MvPolynomial ι R))
    (P.relation x)
have rw : (↑(MvPolynomial.coeffs (P.relation x)) : Set R) ⊆ Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R)
Tactic: rw [MvPolynomial.mem_range_map_iff_coeffs_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
r : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S)
        (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
      S)
    (0 : S)
have rw : Eq.{u_2 + 1} (α := S)
  ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S)
      ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
          (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
        MvPolynomial ι R) :
    S)
  (0 : S)
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, map_relationOfHasCoeffs, aeval_val_relation]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
r : σ
rw :
  Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S)
        ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
            (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
          MvPolynomial ι R) :
      S)
    (0 : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S)
        (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
      S)
    (0 : S)
have rw₁ : Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) (P.relation r) : S) (0 : S)
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, map_relationOfHasCoeffs, aeval_val_relation]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
r : σ
rw :
  Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S)
        ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
            (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
          MvPolynomial ι R) :
      S)
    (0 : S)
rw₁ : Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) (P.relation r) : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S)
        (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
      S)
    (0 : S)
have rw₂ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, map_relationOfHasCoeffs, aeval_val_relation]