case h.h
R : Type u_4
inst✝²³ : CommSemiring R
R₂ : Type u_6
inst✝²² : CommSemiring R₂
R₃ : Type u_5
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.460205
inst✝²⁰ : CommSemiring R₄
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type ?u.460220
Mₗ : Type ?u.460223
Nₗ : Type ?u.460226
Pₗ : Type ?u.460229
Qₗ : Type ?u.460232
Qₗ' : Type ?u.460235
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
x✝¹ : M
x✝ : N
⊢ ↑(↑(compl₂ f id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
R : Type u_4
inst✝²³ : CommSemiring R
R₂ : Type u_6
inst✝²² : CommSemiring R₂
R₃ : Type u_5
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.460205
inst✝²⁰ : CommSemiring R₄
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type ?u.460220
Mₗ : Type ?u.460223
Nₗ : Type ?u.460226
Pₗ : Type ?u.460229
Qₗ : Type ?u.460232
Qₗ' : Type ?u.460235
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
⊢ compl₂ f id = f
ext
no goals
case h.h
R : Type u_4
inst✝²³ : CommSemiring R
R₂ : Type u_6
inst✝²² : CommSemiring R₂
R₃ : Type u_5
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.460205
inst✝²⁰ : CommSemiring R₄
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type ?u.460220
Mₗ : Type ?u.460223
Nₗ : Type ?u.460226
Pₗ : Type ?u.460229
Qₗ : Type ?u.460232
Qₗ' : Type ?u.460235
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
x✝¹ : M
x✝ : N
⊢ ↑(↑(compl₂ f id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
rw [compl₂_apply, id_coe, id.def]