case mp
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
⊢ f₁ = f₂

case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : f₁ = f₂
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g' ↔ f₁ = f₂
constructor <;> intro h
case mp.h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
case mp
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
⊢ f₁ = f₂
ext (x y)
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
x' : Qₗ
hx : ↑g x' = x
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
case mp.h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
cases' hₗ x with x' hx
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
x' : Qₗ
hx : ↑g x' = x
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
subst hx
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
y' : Qₗ'
hy : ↑g' y' = y
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
cases' hᵣ y with y' hy
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ ↑(↑f₁ (↑g x')) (↑g' y') = ↑(↑f₂ (↑g x')) (↑g' y')
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
y' : Qₗ'
hy : ↑g' y' = y
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
subst hy
no goals
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ ↑(↑f₁ (↑g x')) (↑g' y') = ↑(↑f₂ (↑g x')) (↑g' y')
convert LinearMap.congr_fun₂ h x' y' using 0
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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ₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₁ g g'
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : f₁ = f₂
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
subst h
no goals
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type ?u.489611
inst✝²² : CommSemiring R₂
R₃ : Type ?u.489617
inst✝²¹ : CommSemiring R₃
R₄ : Type ?u.489623
inst✝²⁰ : CommSemiring R₄
M : Type ?u.489629
N : Type ?u.489632
P : Type ?u.489635
Q : Type ?u.489638
Mₗ : Type u_2
Nₗ : Type u_4
Pₗ : Type u_3
Qₗ : Type u_5
Qₗ' : Type u_6
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ₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₁ g g'
rfl