Theorem: Submodule_cutspace (src/Cutspace.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ ∃ H_, Set.Finite H_ ∧ ↑p = cutSpace H_
Tactic:
use Submodule_cut p
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Submodule_cut p) ∧ ↑p = cutSpace (Submodule_cut p)

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Submodule_cut p) ∧ ↑p = cutSpace (Submodule_cut p)
Tactic:
use Submodule_cut_finite p
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ ↑p = cutSpace (Submodule_cut p)

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ ↑p = cutSpace (Submodule_cut p)
Tactic:
ext x
State after:
case right.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p ↔ x ∈ cutSpace (Submodule_cut p)

State before:
case right.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p ↔ x ∈ cutSpace (Submodule_cut p)
Tactic:
constructor
State after:
case right.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p → x ∈ cutSpace (Submodule_cut p)

case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ cutSpace (Submodule_cut p) → x ∈ ↑p

State before:
case right.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p → x ∈ cutSpace (Submodule_cut p)
Tactic:
rintro hx Hi_ ⟨ H, ⟨ _, ⟨ v, ⟨ i, hi ⟩, rfl ⟩ , hHHalfpair ⟩, rfl ⟩
State after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ x ∈ ↑H

State before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ x ∈ ↑H
Tactic:
rw [Halfspace_mem]
State after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ ↑H.f x ≤ H.α

State before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ ↑H.f x ≤ H.α
Tactic:
revert hHHalfpair H
State after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ ∀ H ∈ orthoHyperplane v, ↑H.f x ≤ H.α

State before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ ∀ H ∈ orthoHyperplane v, ↑H.f x ≤ H.α
Tactic:
rw [← mem_cutSpace,  orthoHyperplane_mem, ← hi, Submodule.inner_left_of_mem_orthogonal hx]
State after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i ∈ pᗮ

State before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i ∈ pᗮ
Tactic:
exact Submodule.coe_mem ((FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i)
State after:
no goals

State before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ cutSpace (Submodule_cut p) → x ∈ ↑p
Tactic:
rintro hHi_
State after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : x ∈ cutSpace (Submodule_cut p)
⊢ x ∈ ↑p

State before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : x ∈ cutSpace (Submodule_cut p)
⊢ x ∈ ↑p
Tactic:
rw [Submodule_cut, orthoHyperplanes_mem] at hHi_
State after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ ↑p

State before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ ↑p
Tactic:
rw [SetLike.mem_coe, ← Submodule.orthogonal_orthogonal p]
State after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ pᗮᗮ

State before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ pᗮᗮ
Tactic:
intro y hy
State after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
⊢ ⟪y, x⟫_ℝ = 0

State before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
⊢ ⟪y, x⟫_ℝ = 0
Tactic:
have : ∀ i, inner (Subtype.val (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ } i)) x = (0:ℝ) := by
  intro i
  let v : E := (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i
  let v' : { x // x ≠ 0 } := ⟨ v, fun hv => (Basis.ne_zero (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i) (Submodule.coe_eq_zero.mp hv) ⟩
  exact hHi_ v' ⟨ i, rfl ⟩
State after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : ∀ (i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)), ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
⊢ ⟪y, x⟫_ℝ = 0

State before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : ∀ (i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)), ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
⊢ ⟪y, x⟫_ℝ = 0
Tactic:
rw [← Submodule.mem_orthogonal_Basis] at this
State after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : x ∈ pᗮᗮ
⊢ ⟪y, x⟫_ℝ = 0

State before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : x ∈ pᗮᗮ
⊢ ⟪y, x⟫_ℝ = 0
Tactic:
exact this _ hy
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
⊢ ∀ (i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)), ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
intro i
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
let v : E := (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
let v' : { x // x ≠ 0 } := ⟨ v, fun hv => (Basis.ne_zero (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i) (Submodule.coe_eq_zero.mp hv) ⟩
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
v' : { x // x ≠ 0 } := { val := v, property := ⋯ }
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
v' : { x // x ≠ 0 } := { val := v, property := ⋯ }
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
exact hHi_ v' ⟨ i, rfl ⟩
State after:
no goals