-- Mathlib/RingTheory/Presentation.lean
private lemma aux_surjective : Function.Surjective (Q.aux P) := fun p ↦ by
  induction' p using MvPolynomial.induction_on with a p q hp hq p i h
  · use rename Sum.inr <| P.σ a
    simp only [aux, aeval_rename, Sum.elim_comp_inr]
    have (p : MvPolynomial P.vars R) :
        aeval (C ∘ P.val) p = (C (aeval P.val p) : MvPolynomial Q.vars S)

Proof state:
case h_add
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
p q : MvPolynomial P.vars R
hp : (aeval (⇑C ∘ P.val)) p = C ((aeval P.val) p)
hq : (aeval (⇑C ∘ P.val)) q = C ((aeval P.val) q)
⊢ (aeval (⇑C ∘ P.val)) (p + q) = C ((aeval P.val) (p + q))

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
i : Q.vars
a : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ (Algebra.Presentation.aux Q P) (a * X (Sum.inl i)) = (Algebra.Presentation.aux Q P) a * X i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
p : MvPolynomial Q.vars S
⊢ ∃ a, (Algebra.Presentation.aux Q P) a = p

Tactic:
induction' p using MvPolynomial.induction_on with a p q hp hq p i h

Result:
case h_C
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = C a

case h_add
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
p q : MvPolynomial Q.vars S
hp : ∃ a, (Algebra.Presentation.aux Q P) a = p
hq : ∃ a, (Algebra.Presentation.aux Q P) a = q
⊢ ∃ a, (Algebra.Presentation.aux Q P) a = p + q

case h_X
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
p : MvPolynomial Q.vars S
i : Q.vars
h : ∃ a, (Algebra.Presentation.aux Q P) a = p
⊢ ∃ a, (Algebra.Presentation.aux Q P) a = p * X i

Proof state:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
⊢ (Algebra.Presentation.aux Q P) ((rename Sum.inr) (P.σ a)) = C a

Tactic:
simp only [aux, aeval_rename, Sum.elim_comp_inr]

Result:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
⊢ (aeval (⇑C ∘ P.val)) (P.σ a) = C a

Proof state:
case h_add.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a b : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = (Algebra.Presentation.aux Q P) a + (Algebra.Presentation.aux Q P) b

Tactic:
exact ⟨a + b, map_add _ _ _⟩

Result:
no goals

Proof state:
case h_C
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = C a

Tactic:
use rename Sum.inr <| P.σ a

Result:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
⊢ (Algebra.Presentation.aux Q P) ((rename Sum.inr) (P.σ a)) = C a

Proof state:
case h_X
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
p : MvPolynomial P.vars R
i : P.vars
h : (aeval (⇑C ∘ P.val)) p = C ((aeval P.val) p)
⊢ (aeval (⇑C ∘ P.val)) (p * X i) = C ((aeval P.val) (p * X i))

Tactic:
simp [h]

Result:
no goals

Proof state:
case h_C
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a✝ : S
a : R
⊢ (aeval (⇑C ∘ P.val)) (C a) = C ((aeval P.val) (C a))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
p : MvPolynomial P.vars R
⊢ (aeval (⇑C ∘ P.val)) p = C ((aeval P.val) p)

Tactic:
induction' p using MvPolynomial.induction_on with a p q hp hq p i h

Result:
case h_C
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a✝ : S
a : R
⊢ (aeval (⇑C ∘ P.val)) (C a) = C ((aeval P.val) (C a))

case h_add
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
p q : MvPolynomial P.vars R
hp : (aeval (⇑C ∘ P.val)) p = C ((aeval P.val) p)
hq : (aeval (⇑C ∘ P.val)) q = C ((aeval P.val) q)
⊢ (aeval (⇑C ∘ P.val)) (p + q) = C ((aeval P.val) (p + q))

case h_X
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
p : MvPolynomial P.vars R
i : P.vars
h : (aeval (⇑C ∘ P.val)) p = C ((aeval P.val) p)
⊢ (aeval (⇑C ∘ P.val)) (p * X i) = C ((aeval P.val) (p * X i))

Proof state:
case h_X
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
p : MvPolynomial Q.vars S
i : Q.vars
h : ∃ a, (Algebra.Presentation.aux Q P) a = p
⊢ ∃ a, (Algebra.Presentation.aux Q P) a = p * X i

Tactic:
obtain ⟨a, rfl⟩ := h

Result:
case h_X.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
i : Q.vars
a : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = (Algebra.Presentation.aux Q P) a * X i

Proof state:
case h_add
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
p q : MvPolynomial Q.vars S
hp : ∃ a, (Algebra.Presentation.aux Q P) a = p
hq : ∃ a, (Algebra.Presentation.aux Q P) a = q
⊢ ∃ a, (Algebra.Presentation.aux Q P) a = p + q

Tactic:
obtain ⟨a, rfl⟩ := hp

Result:
case h_add.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
q : MvPolynomial Q.vars S
hq : ∃ a, (Algebra.Presentation.aux Q P) a = q
a : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = (Algebra.Presentation.aux Q P) a + q

Proof state:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : S
this : ∀ (p : MvPolynomial P.vars R), (aeval (⇑C ∘ P.val)) p = C ((aeval P.val) p)
⊢ (aeval (⇑C ∘ P.val)) (P.σ a) = C a

Tactic:
simp [this]

Result:
no goals