case h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.481546
inst✝²² : CommSemiring R₂
R₃ : Type ?u.481552
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.481558
inst✝²⁰ : CommSemiring R₄
M : Type ?u.481564
N : Type ?u.481567
P : Type ?u.481570
Q : Type ?u.481573
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type ?u.481585
Qₗ' : Type ?u.481588
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
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x✝¹ : Mₗ
x✝ : Nₗ
⊢ ↑(↑(compl₁₂ f id id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.481546
inst✝²² : CommSemiring R₂
R₃ : Type ?u.481552
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.481558
inst✝²⁰ : CommSemiring R₄
M : Type ?u.481564
N : Type ?u.481567
P : Type ?u.481570
Q : Type ?u.481573
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type ?u.481585
Qₗ' : Type ?u.481588
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
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
⊢ compl₁₂ f id id = f
ext
no goals
case h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.481546
inst✝²² : CommSemiring R₂
R₃ : Type ?u.481552
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.481558
inst✝²⁰ : CommSemiring R₄
M : Type ?u.481564
N : Type ?u.481567
P : Type ?u.481570
Q : Type ?u.481573
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type ?u.481585
Qₗ' : Type ?u.481588
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
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x✝¹ : Mₗ
x✝ : Nₗ
⊢ ↑(↑(compl₁₂ f id id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
simp_rw [compl₁₂_apply, id_coe, id.def]