-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem span_singleton_inf_orthogonal_eq_bot (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂) (x : V₁)
    (hx : ¬B.IsOrtho x x) : (K₁ ∙ x) ⊓ Submodule.orthogonalBilin (K₁ ∙ x) B = ⊥

Proof state:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : J₁' (μ x) • (B x) x = 0
y : J₁' (μ x) = 0
⊢ μ x = 0

Tactic:
simpa using y

Result:
no goals

Proof state:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
⊢ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B = ⊥

Tactic:
refine eq_bot_iff.2 fun y h ↦ ?_

Result:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
y : V₁
h : y ∈ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B
⊢ y ∈ ⊥

Proof state:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : J₁' (μ x) • (B x) x = 0
⊢ μ x = 0

Tactic:
exact Or.elim (smul_eq_zero.mp h)
    (fun y ↦ by simpa using y)
    (fun hfalse ↦ False.elim <| hx hfalse)

Result:
no goals

Proof state:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
⊢ μ x • x ∈ ⊥

Tactic:
suffices hμzero : μ x = 0 by rw [hμzero, zero_smul, Submodule.mem_bot]

Result:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
⊢ μ x = 0

Proof state:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
⊢ μ x = 0

Tactic:
rw [isOrtho_def, map_smulₛₗ] at h

Result:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : J₁' (μ x) • (B x) x = 0
⊢ μ x = 0

Proof state:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B
⊢ x ∈ Submodule.span K₁ ↑{x}

Tactic:
simp [Submodule.mem_span]

Result:
no goals

Proof state:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (∑ i ∈ {x}, μ i • i)
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥

Tactic:
rw [Finset.sum_singleton] at h ⊢

Result:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
⊢ μ x • x ∈ ⊥

Proof state:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
⊢ Submodule.span K₁ {x} ⊓ (Submodule.span K₁ {x}).orthogonalBilin B = ⊥

Tactic:
rw [← Finset.coe_singleton]

Result:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
⊢ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B = ⊥

Proof state:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
y : V₁
h : y ∈ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B
⊢ y ∈ ⊥

Tactic:
rcases mem_span_finset.1 h.1 with ⟨μ, rfl⟩

Result:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥

Proof state:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
hμzero : μ x = 0
⊢ μ x • x ∈ ⊥

Tactic:
rw [hμzero, zero_smul, Submodule.mem_bot]

Result:
no goals

Proof state:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥

Tactic:
replace h := h.2 x (by simp [Submodule.mem_span] : x ∈ Submodule.span K₁ ({x} : Finset V₁))

Result:
case intro
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (∑ i ∈ {x}, μ i • i)
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥