case mp
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
⊢ comp B' f = compl₂ B g

case mpr
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : comp B' f = compl₂ B g
⊢ IsAdjointPair B B' f g
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
⊢ IsAdjointPair B B' f g ↔ comp B' f = compl₂ B g
constructor <;> intro h
case mp.h.h
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
x : M
y : M₁
⊢ ↑(↑(comp B' f) x) y = ↑(↑(compl₂ B g) x) y
case mp
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
⊢ comp B' f = compl₂ B g
ext (x y)
case mp.h.h
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
x : M
y : M₁
⊢ ↑(↑B' (↑f x)) y = ↑(↑B x) (↑g y)
case mp.h.h
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
x : M
y : M₁
⊢ ↑(↑(comp B' f) x) y = ↑(↑(compl₂ B g) x) y
rw [comp_apply, compl₂_apply]
no goals
case mp.h.h
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
x : M
y : M₁
⊢ ↑(↑B' (↑f x)) y = ↑(↑B x) (↑g y)
exact h x y
case mpr
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : comp B' f = compl₂ B g
x✝ : M
y✝ : M₁
⊢ ↑(↑B' (↑f x✝)) y✝ = ↑(↑B x✝) (↑g y✝)
case mpr
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : comp B' f = compl₂ B g
⊢ IsAdjointPair B B' f g
intro _ _
no goals
case mpr
R : Type u_1
R₁ : Type ?u.286879
R₂ : Type ?u.286882
R₃ : Type ?u.286885
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.286894
Mₗ₁ : Type ?u.286897
Mₗ₁' : Type ?u.286900
Mₗ₂ : Type ?u.286903
Mₗ₂' : Type ?u.286906
K : Type ?u.286909
K₁ : Type ?u.286912
K₂ : Type ?u.286915
V : Type ?u.286918
V₁ : Type ?u.286921
V₂ : Type ?u.286924
n : Type ?u.286927
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : comp B' f = compl₂ B g
x✝ : M
y✝ : M₁
⊢ ↑(↑B' (↑f x✝)) y✝ = ↑(↑B x✝) (↑g y✝)
rw [← compl₂_apply, ← comp_apply, h]