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 ι σ
p q : MvPolynomial ι' S
hp : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p
hq : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = q
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p + q
have add : ∀ (a : MvPolynomial (ι' ⊕ ι) R),
  ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
    (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 =
      HAdd.hAdd (α := MvPolynomial ι' S)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a : MvPolynomial ι' S) q
Tactic: obtain ⟨a, rfl⟩ := hp
Cleared hypotheses: p, hp
-- 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 ι σ
q : MvPolynomial ι' S
hq : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = q
a : MvPolynomial (ι' ⊕ ι) R
⊢ ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
    (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 =
      HAdd.hAdd (α := MvPolynomial ι' S)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a : MvPolynomial ι' S) q
have add : ∀ (b : MvPolynomial (ι' ⊕ ι) R),
  ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
    (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 =
      HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a : MvPolynomial ι' S)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) b : MvPolynomial ι' S)
Tactic: obtain ⟨b, rfl⟩ := hq
Cleared hypotheses: q, hq
-- 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 ι σ
p : MvPolynomial ι' S
i : ι'
h : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p * X i
have mul_X : ∀ (a : MvPolynomial (ι' ⊕ ι) R),
  ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
    (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 =
      HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a : MvPolynomial ι' S) (X i)
Tactic: obtain ⟨a, rfl⟩ := h
Cleared hypotheses: p, h
-- 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 ι σ
p : MvPolynomial ι' S
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p
have C : ∀ (a : S),
  ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
    Eq (α := MvPolynomial ι' S) ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 : MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
    use rename Sum.inr <| P.σ a
    simp [aux, aeval_rename]
  | add p q hp hq =>
    obtain ⟨a, rfl⟩ := hp
    obtain ⟨b, rfl⟩ := hq
    exact ⟨a + b, map_add _ _ _⟩
  | mul_X p i h =>
    obtain ⟨a, rfl⟩ := h
    exact ⟨(a * X (Sum.inl i)), by simp⟩
Cleared hypotheses: 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 ι σ
p : MvPolynomial ι' S
C :
  ∀ (a : S),
    ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
      Eq (α := MvPolynomial ι' S)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 : MvPolynomial ι' S)
        ((MvPolynomial.C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p
have add : ∀ (p q : MvPolynomial ι' S)
  (hp : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p)
  (hq : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = q),
  ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p + q
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
    use rename Sum.inr <| P.σ a
    simp [aux, aeval_rename]
  | add p q hp hq =>
    obtain ⟨a, rfl⟩ := hp
    obtain ⟨b, rfl⟩ := hq
    exact ⟨a + b, map_add _ _ _⟩
  | mul_X p i h =>
    obtain ⟨a, rfl⟩ := h
    exact ⟨(a * X (Sum.inl i)), by simp⟩
Cleared hypotheses: 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 ι σ
p : MvPolynomial ι' S
C :
  ∀ (a : S),
    ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
      Eq (α := MvPolynomial ι' S)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 : MvPolynomial ι' S)
        ((MvPolynomial.C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
add :
  ∀ (p q : MvPolynomial ι' S)
    (hp : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p)
    (hq : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = q),
    ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p + q
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p
have mul_X : ∀ (p : MvPolynomial ι' S) (i : ι')
  (h : ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p),
  ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p * X i
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
    use rename Sum.inr <| P.σ a
    simp [aux, aeval_rename]
  | add p q hp hq =>
    obtain ⟨a, rfl⟩ := hp
    obtain ⟨b, rfl⟩ := hq
    exact ⟨a + b, map_add _ _ _⟩
  | mul_X p i h =>
    obtain ⟨a, rfl⟩ := h
    exact ⟨(a * X (Sum.inl i)), by simp⟩
Cleared hypotheses: 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 ι σ
⊢ (⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P) =
    Set.range Q.relation
have h : ∀ (x : MvPolynomial ι' S),
  Membership.mem (γ := Set (MvPolynomial ι' S))
      ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) x ↔
    x ∈ Set.range Q.relation
Tactic: ext x
-- 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 ι σ
x : MvPolynomial ι' S
⊢ Membership.mem (γ := Set (MvPolynomial ι' S))
      ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) x ↔
    x ∈ Set.range Q.relation
have h : Membership.mem (γ := Set (MvPolynomial ι' S))
    ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) x →
  x ∈ Set.range Q.relation
Tactic: constructor
-- 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 ι σ
x : MvPolynomial ι' S
h :
  Membership.mem (γ := Set (MvPolynomial ι' S))
      ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) x →
    x ∈ Set.range Q.relation
⊢ Membership.mem (γ := Set (MvPolynomial ι' S))
      ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) x ↔
    x ∈ Set.range Q.relation
have h₁ : x ∈ Set.range Q.relation →
  Membership.mem (γ := Set (MvPolynomial ι' S))
    ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) x
Tactic: constructor
-- 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 ι σ
y : σ'
⊢ Membership.mem (γ := Set (MvPolynomial ι' S))
    ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) (Q.relation y)
have h : Q.compRelationAux P y ∈ Set.range (Q.compRelationAux P) ∧
  (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (Q.compRelationAux P y) = Q.relation y
Tactic: use Q.compRelationAux P y
-- 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 ι σ
⊢ Q.aux P =
    AlgHom.comp (mapAlgHom (aeval P.val))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
have hf : ∀ (i : ι' ⊕ ι),
  Eq (α := MvPolynomial ι' S) ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S)
    ((AlgHom.comp (mapAlgHom (aeval P.val))
            (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (X i) :
      MvPolynomial ι' S)
Tactic: ext i : 1
-- 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 ι σ
i : ι' ⊕ ι
⊢ Eq (α := MvPolynomial ι' S) ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S)
    ((AlgHom.comp (mapAlgHom (aeval P.val))
            (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (X i) :
      MvPolynomial ι' S)
have hf : ∀ (val : ι'),
  Eq (α := MvPolynomial ι' S)
    ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inl val)) : MvPolynomial ι' S)
    ((AlgHom.comp (mapAlgHom (aeval P.val))
            (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (X (Sum.inl val)) :
      MvPolynomial ι' S)
Tactic: cases i
Cleared hypotheses: i
-- 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 ι σ
i : ι' ⊕ ι
hf :
  ∀ (val : ι'),
    Eq (α := MvPolynomial ι' S)
      ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inl val)) : MvPolynomial ι' S)
      ((AlgHom.comp (mapAlgHom (aeval P.val))
              (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
            (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
          (X (Sum.inl val)) :
        MvPolynomial ι' S)
⊢ Eq (α := MvPolynomial ι' S) ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S)
    ((AlgHom.comp (mapAlgHom (aeval P.val))
            (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (X i) :
      MvPolynomial ι' S)
have hf₁ : ∀ (val : ι),
  Eq (α := MvPolynomial ι' S)
    ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inr val)) : MvPolynomial ι' S)
    ((AlgHom.comp (mapAlgHom (aeval P.val))
            (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (X (Sum.inr val)) :
      MvPolynomial ι' S)
Tactic: cases i
Cleared hypotheses: i
-- 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 ι σ
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R)) (RingHom.ker (Q.aux P))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))
have rw : Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
  (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
    (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
    (Ideal.map (F := MvPolynomial ι R →+* MvPolynomial ι' (MvPolynomial ι R)) C
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
  (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
    (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))
Tactic: rw [aux_eq_comp, ← AlgHom.comap_ker, MvPolynomial.ker_mapAlgHom]
-- 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 ι σ
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (Ideal.map (F := MvPolynomial ι R →+* MvPolynomial ι' (MvPolynomial ι R)) C
        (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))
have change : Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
  (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
    (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (IsScalarTower.toAlgHom R (MvPolynomial ι R) (MvPolynomial ι' (MvPolynomial ι R)))
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
  (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
    (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))
Tactic: change Ideal.comap _ (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial ι R) _) _) = _
-- 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 ι σ
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
        (IsScalarTower.toAlgHom R (MvPolynomial ι R) (MvPolynomial ι' (MvPolynomial ι R)))
        (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))
have hf : Function.Bijective (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial ι' (MvPolynomial ι R))
  (⇑(↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
    (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' (MvPolynomial ι R))
Tactic: rw [← sumAlgEquiv_comp_rename_inr, ← Ideal.map_mapₐ, Ideal.comap_map_of_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
ι' : 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 (α := MvPolynomial (ι' ⊕ ι) R →ₐ[R] T) (aeval (Generators.val (Q.comp P.toGenerators)))
    (AlgHom.comp (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Q.aux P))
have hf : ∀ (i : ι' ⊕ ι),
  Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
    ((AlgHom.comp (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (X i) :
      T)
Tactic: ext i
-- 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
i : ι' ⊕ ι
⊢ Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
    ((AlgHom.comp (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (X i) :
      T)
have hf : Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
  ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
      ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S) :
    T)
Tactic: simp only [AlgHom.coe_comp, Function.comp_apply]
-- 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
i : ι' ⊕ ι
⊢ Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S) :
      T)
have hf : ∀ (val : ι'),
  Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inl val)) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inl val)) : MvPolynomial ι' S) :
      T)
Tactic: cases i
Cleared hypotheses: i
-- 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
i : ι' ⊕ ι
hf :
  ∀ (val : ι'),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inl val)) : T)
      ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
          ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inl val)) : MvPolynomial ι' S) :
        T)
⊢ Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S) :
      T)
have hf₁ : ∀ (val : ι),
  Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inr val)) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inr val)) : MvPolynomial ι' S) :
      T)
Tactic: cases i
Cleared hypotheses: i
-- 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
⊢ Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))) =
    Generators.ker (Q.comp P.toGenerators)
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.comap (Q.aux P)
    (RingHom.ker (F := MvPolynomial ι' S →ₐ[R] T) (aevalTower (IsScalarTower.toAlgHom R S T) Q.val)))
Tactic: rw [Generators.ker_eq_ker_aeval_val, Q.aeval_comp_val_eq, ← AlgHom.comap_ker]