case h
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ y ∈ orthogonal B (Submodule.span K {x}) ↔ y ∈ LinearMap.ker (↑(↑toLin B) x)
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
⊢ orthogonal B (Submodule.span K {x}) = LinearMap.ker (↑(↑toLin B) x)
ext y
case h
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y) ↔ ↑(↑(↑toLin B) x) y = 0
case h
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ y ∈ orthogonal B (Submodule.span K {x}) ↔ y ∈ LinearMap.ker (↑(↑toLin B) x)
simp_rw [mem_orthogonal_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]
case h.mp
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y) → ↑(↑(↑toLin B) x) y = 0

case h.mpr
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ ↑(↑(↑toLin B) x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y
case h
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y) ↔ ↑(↑(↑toLin B) x) y = 0
constructor
no goals
case h.mp
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y) → ↑(↑(↑toLin B) x) y = 0
exact fun h => h x ⟨1, one_smul _ _⟩
case h.mpr.intro
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
h : ↑(↑(↑toLin B) x) y = 0
z : K
⊢ IsOrtho B (z • x) y
case h.mpr
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
⊢ ↑(↑(↑toLin B) x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y
rintro h _ ⟨z, rfl⟩
case h.mpr.intro
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
h : ↑(↑(↑toLin B) x) y = 0
z : K
⊢ z = 0 ∨ bilin B x y = 0
case h.mpr.intro
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
h : ↑(↑(↑toLin B) x) y = 0
z : K
⊢ IsOrtho B (z • x) y
rw [IsOrtho, smul_left, mul_eq_zero]
no goals
case h.mpr.intro
R : Type ?u.1290200
M : Type ?u.1290203
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1290239
M₁ : Type ?u.1290242
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1290851
M₂ : Type ?u.1290854
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1291041
M₃ : Type ?u.1291044
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x y : V
h : ↑(↑(↑toLin B) x) y = 0
z : K
⊢ z = 0 ∨ bilin B x y = 0
exact Or.intro_right _ h