R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.117040
R₃ : Type ?u.117043
M : Type ?u.117046
M₁ : Type u_3
M₂ : Type ?u.117052
Mₗ₁ : Type ?u.117055
Mₗ₁' : Type ?u.117058
Mₗ₂ : Type ?u.117061
Mₗ₂' : Type ?u.117064
K : Type ?u.117067
K₁ : Type ?u.117070
K₂ : Type ?u.117073
V : Type ?u.117076
V₁ : Type ?u.117079
V₂ : Type ?u.117082
n : Type ?u.117085
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
x✝ : M₁
hx : ↑(flip B) x✝ = 0
⊢ ↑B x✝ = 0
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.117040
R₃ : Type ?u.117043
M : Type ?u.117046
M₁ : Type u_3
M₂ : Type ?u.117052
Mₗ₁ : Type ?u.117055
Mₗ₁' : Type ?u.117058
Mₗ₂ : Type ?u.117061
Mₗ₂' : Type ?u.117064
K : Type ?u.117067
K₁ : Type ?u.117070
K₂ : Type ?u.117073
V : Type ?u.117076
V₁ : Type ?u.117079
V₂ : Type ?u.117082
n : Type ?u.117085
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
⊢ ker (flip B) = ⊥
refine' ker_eq_bot'.mpr fun _ hx ↦ ker_eq_bot'.mp h _ _
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.117040
R₃ : Type ?u.117043
M : Type ?u.117046
M₁ : Type u_3
M₂ : Type ?u.117052
Mₗ₁ : Type ?u.117055
Mₗ₁' : Type ?u.117058
Mₗ₂ : Type ?u.117061
Mₗ₂' : Type ?u.117064
K : Type ?u.117067
K₁ : Type ?u.117070
K₂ : Type ?u.117073
V : Type ?u.117076
V₁ : Type ?u.117079
V₂ : Type ?u.117082
n : Type ?u.117085
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
x✝¹ : M₁
hx : ↑(flip B) x✝¹ = 0
x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = ↑0 x✝
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.117040
R₃ : Type ?u.117043
M : Type ?u.117046
M₁ : Type u_3
M₂ : Type ?u.117052
Mₗ₁ : Type ?u.117055
Mₗ₁' : Type ?u.117058
Mₗ₂ : Type ?u.117061
Mₗ₂' : Type ?u.117064
K : Type ?u.117067
K₁ : Type ?u.117070
K₂ : Type ?u.117073
V : Type ?u.117076
V₁ : Type ?u.117079
V₂ : Type ?u.117082
n : Type ?u.117085
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
x✝ : M₁
hx : ↑(flip B) x✝ = 0
⊢ ↑B x✝ = 0
ext
no goals
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.117040
R₃ : Type ?u.117043
M : Type ?u.117046
M₁ : Type u_3
M₂ : Type ?u.117052
Mₗ₁ : Type ?u.117055
Mₗ₁' : Type ?u.117058
Mₗ₂ : Type ?u.117061
Mₗ₂' : Type ?u.117064
K : Type ?u.117067
K₁ : Type ?u.117070
K₂ : Type ?u.117073
V : Type ?u.117076
V₁ : Type ?u.117079
V₂ : Type ?u.117082
n : Type ?u.117085
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
x✝¹ : M₁
hx : ↑(flip B) x✝¹ = 0
x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = ↑0 x✝
exact H _ _ (LinearMap.congr_fun hx _)