-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem orthogonal_span_singleton_eq_to_lin_ker {B : V →ₗ[K] V →ₛₗ[J] V₂} (x : V) :
    Submodule.orthogonalBilin (K ∙ x) B = LinearMap.ker (B x)

Proof state:
case h.mpr.intro
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ (RingHom.id K) z = 0 ∨ (B x) y = 0

Tactic:
exact Or.intro_right _ h

Result:
no goals

Proof state:
case h
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ y ∈ (Submodule.span K {x}).orthogonalBilin B ↔ y ∈ ker (B x)

Tactic:
simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]

Result:
case h
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) ↔ (B x) y = 0

Proof state:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x : V
⊢ (Submodule.span K {x}).orthogonalBilin B = ker (B x)

Tactic:
ext y

Result:
case h
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ y ∈ (Submodule.span K {x}).orthogonalBilin B ↔ y ∈ ker (B x)

Proof state:
case h.mp
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) → (B x) y = 0

Tactic:
exact fun h ↦ h x ⟨1, one_smul _ _⟩

Result:
no goals

Proof state:
case h.mpr.intro
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ B.IsOrtho (z • x) y

Tactic:
rw [isOrtho_def, map_smulₛₗ₂, smul_eq_zero]

Result:
case h.mpr.intro
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ (RingHom.id K) z = 0 ∨ (B x) y = 0

Proof state:
case h.mpr
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (B x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y

Tactic:
rintro h _ ⟨z, rfl⟩

Result:
case h.mpr.intro
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ B.IsOrtho (z • x) y

Proof state:
case h
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) ↔ (B x) y = 0

Tactic:
constructor

Result:
case h.mp
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) → (B x) y = 0

case h.mpr
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (B x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y