-- Mathlib/RingTheory/Presentation.lean
private lemma aux_image_relation :
    Q.aux P '' (Set.range (Algebra.Presentation.comp_relation_aux Q P)) = Set.range Q.relation

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P) = Set.range Q.relation

Tactic:
ext x

Result:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
x : MvPolynomial Q.vars S
⊢ x ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P) ↔
    x ∈ Set.range Q.relation

Proof state:
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
x : MvPolynomial Q.vars S
⊢ x ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P) →
    x ∈ Set.range Q.relation

Tactic:
rintro ⟨y, ⟨a, rfl⟩, rfl⟩

Result:
case h.mp.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : Q.rels
⊢ (Algebra.Presentation.aux Q P) (Algebra.Presentation.comp_relation_aux Q P a) ∈ Set.range Q.relation

Proof state:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
x : MvPolynomial Q.vars S
⊢ x ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P) ↔
    x ∈ Set.range Q.relation

Tactic:
constructor

Result:
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
x : MvPolynomial Q.vars S
⊢ x ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P) →
    x ∈ Set.range Q.relation

case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
x : MvPolynomial Q.vars S
⊢ x ∈ Set.range Q.relation →
    x ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P)

Proof state:
case h.mp.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a : Q.rels
⊢ (Algebra.Presentation.aux Q P) (Algebra.Presentation.comp_relation_aux Q P a) ∈ Set.range Q.relation

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

Result:
no goals

Proof state:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
y : Q.rels
⊢ Algebra.Presentation.comp_relation_aux Q P y ∈ Set.range (Algebra.Presentation.comp_relation_aux Q P) ∧
    (Algebra.Presentation.aux Q P) (Algebra.Presentation.comp_relation_aux Q P y) = Q.relation y

Tactic:
simp only [Set.mem_range, exists_apply_eq_apply, true_and, comp_relation_aux_map]

Result:
no goals

Proof state:
case h.mpr.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
y : Q.rels
⊢ Q.relation y ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P)

Tactic:
use Q.comp_relation_aux P y

Result:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
y : Q.rels
⊢ Algebra.Presentation.comp_relation_aux Q P y ∈ Set.range (Algebra.Presentation.comp_relation_aux Q P) ∧
    (Algebra.Presentation.aux Q P) (Algebra.Presentation.comp_relation_aux Q P y) = Q.relation y

Proof state:
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
x : MvPolynomial Q.vars S
⊢ x ∈ Set.range Q.relation →
    x ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P)

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mpr.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_2
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
y : Q.rels
⊢ Q.relation y ∈ ⇑(Algebra.Presentation.aux Q P) '' Set.range (Algebra.Presentation.comp_relation_aux Q P)