FormalConjecturesForMathlib.Combinatorics.Additive.Coset

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib

@[expose] public section

noncomputable def maxCosetDim (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (A : Set V) : ℕ :=
  sSup { Module.finrank K S.direction | (S : AffineSubspace K V) (_h : (S : Set V) ⊆ A) }

open scoped Pointwise

The maximum coset dimension in the entire vector space $V$ is exactly the dimension of $V$.


theorem maxCosetDim_univ (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] : maxCosetDim K V (Set.univ : Set V) = Module.finrank K V := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ maxCosetDim K V Set.univ = Module.finrank K V
  dsimp [maxCosetDim]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x} = Module.finrank K V
  apply le_antisymmaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x} ≤ Module.finrank K VaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K V ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}
  ·aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x} ≤ Module.finrank K V apply csSup_lea.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}.Nonemptyh₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ ∀ b ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}, b ≤ Module.finrank K V
    ·a.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}.Nonempty use 0hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ 0 ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}
      use ⊥hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ ∃ (_ : ↑⊥ ⊆ Set.univ), Module.finrank K ↥⊥.direction = 0
      simpAll goals completed! 🐙
    ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ ∀ b ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}, b ≤ Module.finrank K V rintro _ ⟨S, _, rfl⟩h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K Vw✝:↑S ⊆ Set.univ⊢ Module.finrank K ↥S.direction ≤ Module.finrank K V
      exact Submodule.finrank_le S.directionAll goals completed! 🐙
  ·aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K V ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x} apply le_csSupa.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ BddAbove {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K V ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}
    ·a.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ BddAbove {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x} use Module.finrank K VhK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K V ∈ upperBounds {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x}
      rintro _ ⟨S, _, rfl⟩hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K Vw✝:↑S ⊆ Set.univ⊢ Module.finrank K ↥S.direction ≤ Module.finrank K V
      exact Submodule.finrank_le S.directionAll goals completed! 🐙
    ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K V ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ Set.univ), Module.finrank K ↥S.direction = x} use ⊤hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ ∃ (_ : ↑⊤ ⊆ Set.univ), Module.finrank K ↥⊤.direction = Module.finrank K V
      refine ⟨Set.subset_univ _, ?_⟩hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K ↥⊤.direction = Module.finrank K V
      rw [AffineSubspace.direction_top,hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K ↥⊤ = Module.finrank K VAll goals completed! 🐙 finrank_tophK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ Module.finrank K V = Module.finrank K VAll goals completed! 🐙]All goals completed! 🐙

The maximum coset dimension in the empty set $\emptyset$ is $0$.


theorem maxCosetDim_empty (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] : maxCosetDim K V (∅ : Set V) = 0 := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ maxCosetDim K V ∅ = 0
  dsimp [maxCosetDim]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
  have h : {Module.finrank K S.direction | (S : AffineSubspace K V) (_h : (S : Set V) ⊆ ∅)} = {0} := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ maxCosetDim K V ∅ = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
    ext xK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vx:ℕ⊢ x ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} ↔ x ∈ {0}K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
    simp only [Set.mem_ofPred_eq, Set.subset_empty_iff, Set.mem_singleton_iff]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vx:ℕ⊢ (∃ S, ∃ (_ : ↑S = ∅), Module.finrank K ↥S.direction = x) ↔ x = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
    constructormpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vx:ℕ⊢ (∃ S, ∃ (_ : ↑S = ∅), Module.finrank K ↥S.direction = x) → x = 0mprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vx:ℕ⊢ x = 0 → ∃ S, ∃ (_ : ↑S = ∅), Module.finrank K ↥S.direction = xK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
    ·mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vx:ℕ⊢ (∃ S, ∃ (_ : ↑S = ∅), Module.finrank K ↥S.direction = x) → x = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0 rintro ⟨S, hS, rfl⟩mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
      have hbot : S = ⊥ := SetLike.ext'_iff.mpr (byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅⊢ ↑S = ↑⊥mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅hbot:S = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0 simp [hS]All goals completed! 🐙mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅hbot:S = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0)mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅hbot:S = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
      rw [hbot,mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅hbot:S = ⊥⊢ Module.finrank K ↥⊥.direction = 0All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0 AffineSubspace.direction_bot,mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅hbot:S = ⊥⊢ Module.finrank K ↥⊥ = 0All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0 finrank_botmpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VhS:↑S = ∅hbot:S = ⊥⊢ 0 = 0All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0]All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
    ·mprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vx:ℕ⊢ x = 0 → ∃ S, ∃ (_ : ↑S = ∅), Module.finrank K ↥S.direction = xK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0 rintro rflmprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ ∃ S, ∃ (_ : ↑S = ∅), Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
      use ⊥hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K V⊢ ∃ (_ : ↑⊥ = ∅), Module.finrank K ↥⊥.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
      simpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = 0
  rw [h,K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {0} = 0All goals completed! 🐙 csSup_singletonK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ ∅), Module.finrank K ↥S.direction = x} = {0}⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

If $A \subseteq B$, then the maximum coset dimension achievable in $A$ cannot exceed the maximum coset dimension achievable in $B$.

theorem maxCosetDim_mono (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] {A B : Set V} (h : A ⊆ B) :
    maxCosetDim K V A ≤ maxCosetDim K V B := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ maxCosetDim K V A ≤ maxCosetDim K V B
  dsimp [maxCosetDim]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x} ≤
  sSup {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x}
  -- We show that any dimension achievable in A is bounded by the supremum in B
  apply csSup_leh₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}.Nonemptyh₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ ∀ b ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x},
  b ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x}
  ·h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}.Nonempty use 0hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ 0 ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}
    use ⊥hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ ∃ (_ : ↑⊥ ⊆ A), Module.finrank K ↥⊥.direction = 0
    simp [Set.empty_subset]All goals completed! 🐙
  ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ B⊢ ∀ b ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x},
  b ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x} rintro d ⟨S, hS, rfl⟩h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ A⊢ Module.finrank K ↥S.direction ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x}
    apply le_csSuph₂.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ A⊢ BddAbove {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x}h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ A⊢ Module.finrank K ↥S.direction ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x}
    ·h₂.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ A⊢ BddAbove {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x} -- Prove the set of dimensions in B is bounded above
      use Module.finrank K VhK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ A⊢ Module.finrank K V ∈ upperBounds {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x}
      rintro _ ⟨S', _, rfl⟩hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ AS':AffineSubspace K Vw✝:↑S' ⊆ B⊢ Module.finrank K ↥S'.direction ≤ Module.finrank K V
      exact Submodule.finrank_le S'.directionAll goals completed! 🐙
    ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ A⊢ Module.finrank K ↥S.direction ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = x} -- The witness S in A is also a witness in B
      use ShK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VA:Set VB:Set Vh:A ⊆ BS:AffineSubspace K VhS:↑S ⊆ A⊢ ∃ (_ : ↑S ⊆ B), Module.finrank K ↥S.direction = Module.finrank K ↥S.direction
      exact ⟨Set.Subset.trans hS h, rfl⟩All goals completed! 🐙

If the target set $A$ is already an affine subspace, the function returns exactly the rank of its direction.

theorem maxCosetDim_affineSubspace (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (S : AffineSubspace K V) :
    maxCosetDim K V (S : Set V) = Module.finrank K S.direction := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ maxCosetDim K V ↑S = Module.finrank K ↥S.direction
  dsimp [maxCosetDim]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ sSup {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x} = Module.finrank K ↥S.direction
  apply le_antisymmaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ sSup {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x} ≤ Module.finrank K ↥S.directionaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ Module.finrank K ↥S.direction ≤ sSup {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}
  ·aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ sSup {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x} ≤ Module.finrank K ↥S.direction apply csSup_lea.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}.Nonemptyh₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ ∀ b ∈ {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}, b ≤ Module.finrank K ↥S.direction
    ·a.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}.Nonempty use 0hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ 0 ∈ {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}
      use ⊥hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ ∃ (_ : ↑⊥ ⊆ ↑S), Module.finrank K ↥⊥.direction = 0
      simp [Set.empty_subset]All goals completed! 🐙
    ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ ∀ b ∈ {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}, b ≤ Module.finrank K ↥S.direction rintro _ ⟨S', hS', rfl⟩h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VS':AffineSubspace K VhS':↑S' ⊆ ↑S⊢ Module.finrank K ↥S'.direction ≤ Module.finrank K ↥S.direction
      exact Submodule.finrank_mono (AffineSubspace.direction_le hS')All goals completed! 🐙
  ·aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ Module.finrank K ↥S.direction ≤ sSup {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x} apply le_csSupa.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ BddAbove {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ Module.finrank K ↥S.direction ∈ {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}
    ·a.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ BddAbove {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x} use Module.finrank K VhK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ Module.finrank K V ∈ upperBounds {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x}
      rintro _ ⟨S', _, rfl⟩hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K VS':AffineSubspace K Vw✝:↑S' ⊆ ↑S⊢ Module.finrank K ↥S'.direction ≤ Module.finrank K V
      exact Submodule.finrank_le S'.directionAll goals completed! 🐙
    ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K VS:AffineSubspace K V⊢ Module.finrank K ↥S.direction ∈ {x | ∃ S_1, ∃ (_ : ↑S_1 ⊆ ↑S), Module.finrank K ↥S_1.direction = x} use SAll goals completed! 🐙

Similar to the empty set, a set containing exactly one vector should yield a maximum dimension of 0.


theorem maxCosetDim_singleton (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (v : V) : maxCosetDim K V ({v} : Set V) = 0 := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:V⊢ maxCosetDim K V {v} = 0
  dsimp [maxCosetDim]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:V⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
  have h : {Module.finrank K S.direction | (S : AffineSubspace K V) (_h : (S : Set V) ⊆ {v})} = {0} := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:V⊢ maxCosetDim K V {v} = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
    ext xK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vx:ℕ⊢ x ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} ↔ x ∈ {0}K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
    simp only [Set.mem_ofPred_eq, Set.mem_singleton_iff]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vx:ℕ⊢ (∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x) ↔ x = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
    constructormpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vx:ℕ⊢ (∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x) → x = 0mprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vx:ℕ⊢ x = 0 → ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = xK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
    ·mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vx:ℕ⊢ (∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x) → x = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0 rintro ⟨S, hS, rfl⟩mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
      obtain rfl | h_nonempty := eq_bot_or_bot_lt Smp.inlK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VhS:↑⊥ ⊆ {v}⊢ Module.finrank K ↥⊥.direction = 0mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < S⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
      ·mp.inlK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VhS:↑⊥ ⊆ {v}⊢ Module.finrank K ↥⊥.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0 rw [AffineSubspace.direction_bot,mp.inlK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VhS:↑⊥ ⊆ {v}⊢ Module.finrank K ↥⊥ = 0All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0 finrank_botmp.inlK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VhS:↑⊥ ⊆ {v}⊢ 0 = 0All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0]All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
      ·mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < S⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0 have h_dir : S.direction = ⊥ := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:V⊢ maxCosetDim K V {v} = 0mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          apply eq_bot_iff.mprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < S⊢ S.direction ≤ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          rintro y hyK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.direction⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          have h_coe : (S : Set V) ≠ ∅ := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:V⊢ maxCosetDim K V {v} = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
            intro h_empK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_emp:↑S = ∅⊢ FalseK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
            apply ne_of_gt h_nonemptyK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_emp:↑S = ∅⊢ S = ⊥K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
            exact (AffineSubspace.coe_eq_bot_iff S).mp h_empK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          obtain ⟨p, hp⟩ : (S : Set V).Nonempty := Set.nonempty_iff_ne_empty.mpr h_coeK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑S⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          have hpv : p = v := hS hpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑Shpv:p = v⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          have hpy : y +ᵥ p ∈ S := AffineSubspace.vadd_mem_of_mem_direction hy hpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑Shpv:p = vhpy:y +ᵥ p ∈ S⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          have hpyv : y +ᵥ p = v := hS hpyK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑Shpv:p = vhpy:y +ᵥ p ∈ Shpyv:y +ᵥ p = v⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          rw [hpvK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑Shpv:p = vhpy:y +ᵥ p ∈ Shpyv:y +ᵥ v = v⊢ y ∈ ⊥K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑Shpv:p = vhpy:y +ᵥ p ∈ Shpyv:y +ᵥ v = v⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0] at hpyvK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑Shpv:p = vhpy:y +ᵥ p ∈ Shpyv:y +ᵥ v = v⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          change y + v = v at hpyvK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sy:Vhy:y ∈ S.directionh_coe:↑S ≠ ∅p:Vhp:p ∈ ↑Shpv:p = vhpy:y +ᵥ p ∈ Shpyv:y + v = v⊢ y ∈ ⊥mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
          simpa using hpyvmp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
        rw [h_dir,mp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ Module.finrank K ↥⊥ = 0All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0 finrank_botmp.inrK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VS:AffineSubspace K VhS:↑S ⊆ {v}h_nonempty:⊥ < Sh_dir:S.direction = ⊥⊢ 0 = 0All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0]All goals completed! 🐙K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
    ·mprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vx:ℕ⊢ x = 0 → ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = xK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0 rintro rflmprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:V⊢ ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
      use ⊥hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:V⊢ ∃ (_ : ↑⊥ ⊆ {v}), Module.finrank K ↥⊥.direction = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
      simpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = 0
  rw [h,K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ sSup {0} = 0All goals completed! 🐙 csSup_singletonK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:Vh:{x | ∃ S, ∃ (_ : ↑S ⊆ {v}), Module.finrank K ↥S.direction = x} = {0}⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙



lemma maxCosetDim_vadd_le (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (v : V) (A : Set V) :
    maxCosetDim K V (v +ᵥ A) ≤ maxCosetDim K V A := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V (v +ᵥ A) ≤ maxCosetDim K V A
  dsimp [maxCosetDim]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ v +ᵥ A), Module.finrank K ↥S.direction = x} ≤
  sSup {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}
  apply csSup_leh₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ {x | ∃ S, ∃ (_ : ↑S ⊆ v +ᵥ A), Module.finrank K ↥S.direction = x}.Nonemptyh₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ ∀ b ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ v +ᵥ A), Module.finrank K ↥S.direction = x},
  b ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}
  ·h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ {x | ∃ S, ∃ (_ : ↑S ⊆ v +ᵥ A), Module.finrank K ↥S.direction = x}.Nonempty use 0hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ 0 ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ v +ᵥ A), Module.finrank K ↥S.direction = x}
    use ⊥hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ ∃ (_ : ↑⊥ ⊆ v +ᵥ A), Module.finrank K ↥⊥.direction = 0
    simp [Set.empty_subset]All goals completed! 🐙
  ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ ∀ b ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ v +ᵥ A), Module.finrank K ↥S.direction = x},
  b ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x} rintro d ⟨S, hS, rfl⟩h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ A⊢ Module.finrank K ↥S.direction ≤ sSup {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}
    apply le_csSuph₂.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ A⊢ BddAbove {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ A⊢ Module.finrank K ↥S.direction ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}
    ·h₂.h₁K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ A⊢ BddAbove {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x} use Module.finrank K VhK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ A⊢ Module.finrank K V ∈ upperBounds {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}
      rintro _ ⟨S', _, rfl⟩hK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ AS':AffineSubspace K Vw✝:↑S' ⊆ A⊢ Module.finrank K ↥S'.direction ≤ Module.finrank K V
      exact Submodule.finrank_le S'.directionAll goals completed! 🐙
    ·h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ A⊢ Module.finrank K ↥S.direction ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x} let f : V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)h₂K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ Module.finrank K ↥S.direction ∈ {x | ∃ S, ∃ (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}
      refine ⟨S.map (f : V →ᵃ[K] V), ?_, ?_⟩h₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ ↑(AffineSubspace.map (↑f) S) ⊆ Ah₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.direction
      ·h₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ ↑(AffineSubspace.map (↑f) S) ⊆ A rw [AffineSubspace.coe_maph₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ ⇑↑f '' ↑S ⊆ Ah₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ ⇑↑f '' ↑S ⊆ A]h₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ ⇑↑f '' ↑S ⊆ A
        rintro x ⟨y, hy, rfl⟩h₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)y:Vhy:y ∈ ↑S⊢ ↑f y ∈ A
        have h_ya : y ∈ v +ᵥ A := hS hyh₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)y:Vhy:y ∈ ↑Sh_ya:y ∈ v +ᵥ A⊢ ↑f y ∈ A
        rcases h_ya with ⟨a, ha, rfl⟩h₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)a:Vha:a ∈ Ahy:(fun x ↦ v +ᵥ x) a ∈ ↑S⊢ ↑f ((fun x ↦ v +ᵥ x) a) ∈ A
        change -v + (v + a) ∈ Ah₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)a:Vha:a ∈ Ahy:(fun x ↦ v +ᵥ x) a ∈ ↑S⊢ -v + (v + a) ∈ A
        rw [neg_add_cancel_lefth₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)a:Vha:a ∈ Ahy:(fun x ↦ v +ᵥ x) a ∈ ↑S⊢ a ∈ Ah₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)a:Vha:a ∈ Ahy:(fun x ↦ v +ᵥ x) a ∈ ↑S⊢ a ∈ A]h₂.refine_1K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)a:Vha:a ∈ Ahy:(fun x ↦ v +ᵥ x) a ∈ ↑S⊢ a ∈ A
        exact haAll goals completed! 🐙
      ·h₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.direction have hd : (S.map (f : V →ᵃ[K] V)).direction = S.direction := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V (v +ᵥ A) ≤ maxCosetDim K V Ah₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)hd:(AffineSubspace.map (↑f) S).direction = S.direction⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.direction
          rw [AffineSubspace.map_directionK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ Submodule.map (↑f).linear S.direction = S.directionK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ Submodule.map (↑f).linear S.direction = S.directionh₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)hd:(AffineSubspace.map (↑f) S).direction = S.direction⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.direction]K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ Submodule.map (↑f).linear S.direction = S.directionh₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)hd:(AffineSubspace.map (↑f) S).direction = S.direction⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.direction
          change Submodule.map LinearMap.id S.direction = S.directionK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)⊢ Submodule.map LinearMap.id S.direction = S.directionh₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)hd:(AffineSubspace.map (↑f) S).direction = S.direction⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.direction
          exact Submodule.map_id S.directionh₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)hd:(AffineSubspace.map (↑f) S).direction = S.direction⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.directionh₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)hd:(AffineSubspace.map (↑f) S).direction = S.direction⊢ Module.finrank K ↥(AffineSubspace.map (↑f) S).direction = Module.finrank K ↥S.direction
        rw [hdh₂.refine_2K:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set VS:AffineSubspace K VhS:↑S ⊆ v +ᵥ Af:V ≃ᵃ[K] V := AffineEquiv.constVAdd K V (-v)hd:(AffineSubspace.map (↑f) S).direction = S.direction⊢ Module.finrank K ↥S.direction = Module.finrank K ↥S.directionAll goals completed! 🐙]All goals completed! 🐙

Translating a set by a vector does not change its maximum coset dimension.


theorem maxCosetDim_vadd (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (v : V) (A : Set V) :
    maxCosetDim K V (v +ᵥ A) = maxCosetDim K V A := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V (v +ᵥ A) = maxCosetDim K V A
  apply le_antisymmaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V (v +ᵥ A) ≤ maxCosetDim K V AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
  ·aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V (v +ᵥ A) ≤ maxCosetDim K V A exact maxCosetDim_vadd_le K V v AAll goals completed! 🐙
  ·aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A) have h := maxCosetDim_vadd_le K V (-v) (v +ᵥ A)aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
    have h_cancel : -v +ᵥ (v +ᵥ A) = A := byK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set V⊢ maxCosetDim K V (v +ᵥ A) = maxCosetDim K V AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
      ext xK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:V⊢ x ∈ -v +ᵥ v +ᵥ A ↔ x ∈ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
      constructormpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:V⊢ x ∈ -v +ᵥ v +ᵥ A → x ∈ AmprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:V⊢ x ∈ A → x ∈ -v +ᵥ v +ᵥ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
      ·mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:V⊢ x ∈ -v +ᵥ v +ᵥ A → x ∈ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A) rintro ⟨y, ⟨a, ha, rfl⟩, rfl⟩mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)a:Vha:a ∈ A⊢ (fun x ↦ -v +ᵥ x) ((fun x ↦ v +ᵥ x) a) ∈ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
        change -v + (v + a) ∈ AmpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)a:Vha:a ∈ A⊢ -v + (v + a) ∈ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
        rw [neg_add_cancel_leftmpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)a:Vha:a ∈ A⊢ a ∈ AmpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)a:Vha:a ∈ A⊢ a ∈ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)]mpK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)a:Vha:a ∈ A⊢ a ∈ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
        exact haAll goals completed! 🐙aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
      ·mprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:V⊢ x ∈ A → x ∈ -v +ᵥ v +ᵥ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A) rintro hxmprK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ x ∈ -v +ᵥ v +ᵥ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
        use v + xhK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ v + x ∈ v +ᵥ A ∧ (fun x ↦ -v +ᵥ x) (v + x) = xaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
        constructorh.leftK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ v + x ∈ v +ᵥ Ah.rightK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ (fun x ↦ -v +ᵥ x) (v + x) = xaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
        ·h.leftK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ v + x ∈ v +ᵥ AaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A) exact ⟨x, hx, rfl⟩All goals completed! 🐙aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
        ·h.rightK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ (fun x ↦ -v +ᵥ x) (v + x) = xaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A) change -v + (v + x) = xh.rightK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ -v + (v + x) = xaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
          rw [neg_add_cancel_lefth.rightK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)x:Vhx:x ∈ A⊢ x = xaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)]aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V (-v +ᵥ v +ᵥ A) ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
    rw [h_cancelaK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)aK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)] at haK:Type u_1V:Type u_2inst✝³:DivisionRing Kinst✝²:AddCommGroup Vinst✝¹:Module K Vinst✝:FiniteDimensional K Vv:VA:Set Vh:maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)h_cancel:-v +ᵥ v +ᵥ A = A⊢ maxCosetDim K V A ≤ maxCosetDim K V (v +ᵥ A)
    exact hAll goals completed! 🐙