Theorem: origin_Hpolytope (src/Polytope.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = {0}
Tactic:
refine ⟨ ⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range (FiniteDimensional.finBasis ℝ E))), ?_, ?_ ⟩
State after:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))))

case refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Hpolytope ?refine_1 = {0}

State before:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))))
Tactic:
apply Set.Finite.sUnion ?_ (fun t ht => by
  rcases ht with ⟨ x, _, rfl ⟩
  exact orthoHyperplane.Finite _)
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))
Tactic:
apply Set.Finite.image
State after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))

State before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))
Tactic:
apply Set.Finite.preimage (Set.injOn_of_injective Subtype.val_injective _)
State after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Set.range ⇑(FiniteDimensional.finBasis ℝ E))

State before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Set.range ⇑(FiniteDimensional.finBasis ℝ E))
Tactic:
exact Set.finite_range _
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
t : Set (Halfspace E)
ht : t ∈ orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))
⊢ Set.Finite t
Tactic:
rcases ht with ⟨ x, _, rfl ⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
left✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ Set.Finite (orthoHyperplane x)

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
left✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ Set.Finite (orthoHyperplane x)
Tactic:
exact orthoHyperplane.Finite _
State after:
no goals

State before:
case refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Hpolytope ⋯ = {0}
Tactic:
ext x
State after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ {0}

State before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ {0}
Tactic:
rw [Set.mem_singleton_iff]
State after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x = 0

State before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x = 0
Tactic:
change x ∈ cutSpace ( (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ↑(FiniteDimensional.finBasis ℝ E))))) ↔ x = 0
State after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ cutSpace (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))) ↔ x = 0

State before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ cutSpace (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))) ↔ x = 0
Tactic:
rw [orthoHyperplanes_mem]
State after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) ↔ x = 0

State before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) ↔ x = 0
Tactic:
constructor
State after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) → x = 0

case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x = 0 → ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0

State before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) → x = 0
Tactic:
intro h
State after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ x = 0

State before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ x = 0
Tactic:
apply InnerProductSpace.ext_inner_left_basis (FiniteDimensional.finBasis ℝ E)
State after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ ∀ (i : Fin (FiniteDimensional.finrank ℝ E)),
    ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ

State before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ ∀ (i : Fin (FiniteDimensional.finrank ℝ E)),
    ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ
Tactic:
intro i
State after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ

State before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ
Tactic:
rw [inner_zero_right]
State after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0

State before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0
Tactic:
simp only [Set.mem_preimage, Set.mem_range, forall_exists_index, Subtype.forall] at h
State after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
i : Fin (FiniteDimensional.finrank ℝ E)
h :
  ∀ (a : E),
    a ≠ 0 → ∀ (x_1 : Fin (FiniteDimensional.finrank ℝ E)), (FiniteDimensional.finBasis ℝ E) x_1 = a → ⟪a, x⟫_ℝ = 0
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0

State before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
i : Fin (FiniteDimensional.finrank ℝ E)
h :
  ∀ (a : E),
    a ≠ 0 → ∀ (x_1 : Fin (FiniteDimensional.finrank ℝ E)), (FiniteDimensional.finBasis ℝ E) x_1 = a → ⟪a, x⟫_ℝ = 0
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0
Tactic:
exact h (FiniteDimensional.finBasis ℝ E i) (Basis.ne_zero (FiniteDimensional.finBasis ℝ E) i) i rfl
State after:
no goals

State before:
case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x = 0 → ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
Tactic:
rintro rfl x _
State after:
case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
a✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ ⟪↑x, 0⟫_ℝ = 0

State before:
case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
a✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ ⟪↑x, 0⟫_ℝ = 0
Tactic:
rw [inner_zero_right]
State after:
no goals