Theorem: Submodule_cut_finite (src/Cutspace.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Submodule_cut p)
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
p : Subspace ℝ E
⊢ Set.Finite (orthoHyperplane '' (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ))))

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

State before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
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
p : Subspace ℝ E
⊢ Set.Finite (Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))

State before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
Tactic:
apply Set.finite_range
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
t : Set (Halfspace E)
ht : t ∈ orthoHyperplane '' (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
⊢ 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
p : Subspace ℝ E
x : { x // x ≠ 0 }
left✝ : x ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ))
⊢ Set.Finite (orthoHyperplane x)

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