awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
r : σ'
e_g :
  Eq (α := (ι' →₀ ℕ) → S → MvPolynomial ι' S)
    (fun (a : ι' →₀ ℕ) (b : S) ↦
      HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ b) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl a) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)))
    Finsupp.single
⊢ Eq (α := MvPolynomial ι' S)
    (Finsupp.sum (Q.relation r) fun (a : ι' →₀ ℕ) (b : S) ↦
      HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ b) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl a) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)))
    (Finsupp.sum (Q.relation r) Finsupp.single)

Tactic:
congr
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
r : σ'
e_g :
  ∀ (u : ι' →₀ ℕ) (s : S) (m : ι' →₀ ℕ),
    coeff m
        (HMul.hMul (α := MvPolynomial ι' S)
          ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ s) :
            MvPolynomial ι' S)
          (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
            (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
              HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
      coeff m (Finsupp.single u s)
⊢ Eq (α := (ι' →₀ ℕ) → S → MvPolynomial ι' S)
    (fun (a : ι' →₀ ℕ) (b : S) ↦
      HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ b) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl a) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)))
    Finsupp.single

Tactic:
ext u s m
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
e_g :
  coeff m
      (eval₂ (algebraMap R (MvPolynomial ι' S)) ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (P.σ s) *
        HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)) =
    coeff m ((monomial u : (a : S) → MvPolynomial ι' S) s)
⊢ coeff m
      (HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ s) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
    coeff m (Finsupp.single u s)

Tactic:
simp only [MvPolynomial.single_eq_monomial, aeval, AlgHom.coe_mk, coe_eval₂Hom]

Premises used: AlgHom.coe_mk, MvPolynomial.aeval, MvPolynomial.single_eq_monomial, MvPolynomial.coe_eval₂Hom
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
e_g :
  coeff m
      (HMul.hMul (α := MvPolynomial ι' S)
        ((C : (a : S) → MvPolynomial ι' S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ s)) : MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((RingHom.comp C (algebraMap R S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
    coeff m
      (HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((C : (a : S) → MvPolynomial ι' S) s : MvPolynomial ι' S)
        (u.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S))
⊢ coeff m
      (eval₂ (algebraMap R (MvPolynomial ι' S)) ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (P.σ s) *
        HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)) =
    coeff m ((monomial u : (a : S) → MvPolynomial ι' S) s)

Tactic:
rw [monomial_eq, IsScalarTower.algebraMap_eq R S, algebraMap_eq, ← eval₂_comp_left, ← aeval_def]

Premises used: MvPolynomial.aeval_def, IsScalarTower.algebraMap_eq, MvPolynomial.algebraMap_eq, MvPolynomial.monomial_eq, MvPolynomial.eval₂_comp_left
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m
      (HMul.hMul (α := MvPolynomial ι' S)
        ((C : (a : S) → MvPolynomial ι' S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ s)) : MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((RingHom.comp C (algebraMap R S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
    coeff m
      (HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((C : (a : S) → MvPolynomial ι' S) s : MvPolynomial ι' S)
        (u.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S))

Tactic:
simp [Finsupp.prod_mapDomain_index_inj (Sum.inl_injective)]

Premises used: Sum.inl_injective, Finsupp.prod_mapDomain_index_inj
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
a : S
h :
  Eq (α := MvPolynomial ι' S)
    ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ a)) :
      MvPolynomial ι' S)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' 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:
use rename Sum.inr <| P.σ a

Premises used: MvPolynomial.rename, Sum.inr, Algebra.Presentation.toGenerators, Algebra.Generators.σ
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
a : S
⊢ Eq (α := MvPolynomial ι' S)
    ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ a)) :
      MvPolynomial ι' S)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)

Tactic:
simp [aux, aeval_rename]

Premises used: _private.0.Algebra.Presentation.aux, MvPolynomial.aeval_rename
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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
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
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p + q

Tactic:
obtain ⟨a, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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
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)
⊢ ∃ (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 ⟨b, rfl⟩ := hq

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
a 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:
⟨a + b, map_add _ _ _⟩

Premises used: map_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
a 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:
exact ⟨a + b, map_add _ _ _⟩
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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
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)
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p * X i

Tactic:
obtain ⟨a, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 : ι'
a : MvPolynomial (ι' ⊕ ι) R
⊢ (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (a * X (Sum.inl i)) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a : MvPolynomial ι' S) (X i)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 : ι'
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:
exact ⟨(a * X (Sum.inl i)), by simp⟩
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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
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
⊢ ∃ (a : MvPolynomial (ι' ⊕ ι) R), (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a = p

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⟩

Premises used: MvPolynomial.induction_on, MvPolynomial.rename, Sum.inr, _private.0.Algebra.Presentation.aux, MvPolynomial.aeval_rename, MvPolynomial.C, rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
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
⊢ (⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P) =
    Set.range Q.relation

Tactic:
ext x
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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
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
⊢ 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
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
a : σ'
⊢ Membership.mem (α := MvPolynomial ι' S) (Set.range Q.relation)
    ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (Q.compRelationAux P a) : MvPolynomial ι' S)

Tactic:
⟨a, (Q.compRelationAux_map P a).symm⟩

Premises used: Set.Mem, setOf, _private.0.Algebra.Presentation.compRelationAux_map, Exists.intro, Set.range, Eq.symm
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
a : σ'
⊢ Membership.mem (α := MvPolynomial ι' S) (Set.range Q.relation)
    ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (Q.compRelationAux P a) : MvPolynomial ι' S)

Tactic:
exact ⟨a, (Q.compRelationAux_map P a).symm⟩
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 : σ'
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
⊢ Membership.mem (γ := Set (MvPolynomial ι' S))
    ((⇑(Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) '' Set.range (Q.compRelationAux P)) (Q.relation y)

Tactic:
use Q.compRelationAux P y

Premises used: Algebra.Presentation.compRelationAux
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 : σ'
⊢ 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:
simp only [Set.mem_range, exists_apply_eq_apply, true_and, compRelationAux_map]

Premises used: Set.mem_range, _private.0.Algebra.Presentation.compRelationAux_map, true_and, exists_apply_eq_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
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)
⊢ Q.aux P =
    AlgHom.comp (mapAlgHom (aeval P.val))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))

Tactic:
ext i : 1
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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)
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)
⊢ 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:
cases i
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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 ι σ
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:
simp