[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ ↑σ' (↑σ x) = x
[PROOFSTEP]
rw [← RingHom.comp_apply, comp_eq]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ ↑(RingHom.id R₁) x = x
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ ↑σ (↑σ' x) = x
[PROOFSTEP]
rw [← RingHom.comp_apply, comp_eq₂]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ ↑(RingHom.id R₂) x = x
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁴ : Semiring R₁
inst✝³ : Semiring R₂
inst✝² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝¹ : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst✝ : RingHomInvPair σ₁₂ σ₂₁
⊢ RingHom.comp σ₂₁ σ₁₂ = RingHom.id R₁
[PROOFSTEP]
simp only [comp_eq]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁴ : Semiring R₁
inst✝³ : Semiring R₂
inst✝² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝¹ : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst✝ : RingHomInvPair σ₁₂ σ₂₁
⊢ RingHom.comp σ₁₂ σ₂₁ = RingHom.id R₂
[PROOFSTEP]
simp only [comp_eq₂]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ RingHom.comp σ₁₂ (RingHom.id R₁) = σ₁₂
[PROOFSTEP]
ext
[GOAL]
case a
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
x✝ : R₁
⊢ ↑(RingHom.comp σ₁₂ (RingHom.id R₁)) x✝ = ↑σ₁₂ x✝
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ RingHom.comp (RingHom.id R₂) σ₁₂ = σ₁₂
[PROOFSTEP]
ext
[GOAL]
case a
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
x✝ : R₁
⊢ ↑(RingHom.comp (RingHom.id R₂) σ₁₂) x✝ = ↑σ₁₂ x✝
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
⊢ Function.Surjective ↑σ₁₃
[PROOFSTEP]
have := σ₂₃.surjective.comp σ₁₂.surjective
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective (↑σ₂₃ ∘ ↑σ₁₂)
⊢ Function.Surjective ↑σ₁₃
[PROOFSTEP]
rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this 
