awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
inl : IsEmpty ι → Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
inr : Nonempty ι → Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
⊢ Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
h : IsEmpty ι
⊢ Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1

Tactic:
simp [Fintype.card_eq_zero]

Premises used: Fintype.card_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
h : Nonempty ι
inr : Fintype.card ι - 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
⊢ Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1

Tactic:
rw [← tsub_le_iff_right]

Premises used: tsub_le_iff_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
h : Nonempty ι
⊢ Fintype.card ι - 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))

Tactic:
(affineIndependent_iff_le_finrank_vectorSpan _ _
    (tsub_add_cancel_of_le <| Nat.one_le_iff_ne_zero.2 Fintype.card_ne_zero).symm).1 hp

Premises used: Iff.mpr, tsub_add_cancel_of_le, affineIndependent_iff_le_finrank_vectorSpan, Fintype.card_ne_zero, Iff.mp, Nat.one_le_iff_ne_zero, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
h : Nonempty ι
⊢ Fintype.card ι - 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))

Tactic:
exact (affineIndependent_iff_le_finrank_vectorSpan _ _
    (tsub_add_cancel_of_le <| Nat.one_le_iff_ne_zero.2 Fintype.card_ne_zero).symm).1 hp

Premises used: Iff.mpr, tsub_add_cancel_of_le, affineIndependent_iff_le_finrank_vectorSpan, Fintype.card_ne_zero, Iff.mp, Nat.one_le_iff_ne_zero, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
inl :
  ∀ (hs : AffineIndependent k (P := V) (ι := ↥∅) (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Finset V) ∅ x)))
    (hst : (↑∅ : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)), card.{u_2} (α := V) ∅ ≤ #t
inr : ∀ (hs' : s.Nonempty), #s ≤ #t
⊢ #s ≤ #t

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥∅) (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Finset V) ∅ x))
hst : (↑∅ : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
⊢ card.{u_2} (α := V) ∅ ≤ #t

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
inr : ∀ (hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑∅ : Set V)) : Set V)), #s ≤ card.{u_2} (α := V) ∅
inr₁ : ∀ (ht' : t.Nonempty), #s ≤ #t
⊢ #s ≤ #t

Tactic:
obtain rfl | ht' := t.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hs' : s.Nonempty
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑∅ : Set V)) : Set V)
⊢ #s ≤ card.{u_2} (α := V) ∅

Tactic:
simpa [Set.subset_empty_iff] using hst

Premises used: Set.subset_empty_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Nonempty.{u_2 + 1} ↥s

Tactic:
have := hs'.to_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this : Nonempty.{u_2 + 1} ↥s
⊢ Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)

Tactic:
have := ht'.to_set.to_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
⊢ LE.le (α := Submodule k V) (direction (affineSpan k (↑s : Set V)))
    (direction (affineSpan k (↑(affineSpan k (↑t : Set V)) : Set V)))

Tactic:
have direction_le := AffineSubspace.direction_le (affineSpan_mono k hst)
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
direction_le :
  LE.le (α := Submodule k V) (direction (affineSpan k (↑s : Set V)))
    (direction (affineSpan k (↑(affineSpan k (↑t : Set V)) : Set V)))
⊢ LE.le (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))

Tactic:
rw [AffineSubspace.affineSpan_coe, direction_affineSpan, direction_affineSpan,
    ← @Subtype.range_coe _ (s : Set V), ← @Subtype.range_coe _ (t : Set V)] at direction_le

Premises used: direction_affineSpan, Subtype.range_coe, AffineSubspace.affineSpan_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
direction_le :
  LE.le (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))
⊢ finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V))))) +
      1 ≤
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1

Tactic:
have finrank_le := add_le_add_left (Submodule.finrank_mono direction_le) 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
direction_le :
  LE.le (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))
finrank_le :
  finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V))))) +
      1 ≤
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1
⊢ Fintype.card.{u_2} ↥s ≤
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1

Tactic:
erw [hs.finrank_vectorSpan_add_one] at finrank_le

Premises used: AffineIndependent.finrank_vectorSpan_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
direction_le :
  LE.le (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))
finrank_le :
  Fintype.card.{u_2} ↥s ≤
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1
⊢ #s ≤ #t

Tactic:
simpa using finrank_le.trans <| finrank_vectorSpan_range_add_one_le _ _

Premises used: LE.le.trans, finrank_vectorSpan_range_add_one_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
inl :
  ∀ (hs : AffineIndependent k (P := V) (ι := ↥∅) (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Finset V) ∅ x)))
    (hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑∅ : Set V)) (affineSpan k (↑t : Set V))),
    card.{u_2} (α := V) ∅ < #t
inr : ∀ (hs' : s.Nonempty), #s < #t
⊢ #s < #t

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥∅) (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Finset V) ∅ x))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑∅ : Set V)) (affineSpan k (↑t : Set V))
⊢ card.{u_2} (α := V) ∅ < #t

Tactic:
simpa [card_pos] using hst

Premises used: Finset.card_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
inr :
  ∀ (hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑∅ : Set V))),
    #s < card.{u_2} (α := V) ∅
inr₁ : ∀ (ht' : t.Nonempty), #s < #t
⊢ #s < #t

Tactic:
obtain rfl | ht' := t.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hs' : s.Nonempty
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑∅ : Set V))
⊢ #s < card.{u_2} (α := V) ∅

Tactic:
simp at hst
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Nonempty.{u_2 + 1} ↥s

Tactic:
have := hs'.to_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
ht' : t.Nonempty
this : Nonempty.{u_2 + 1} ↥s
⊢ Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)

Tactic:
have := ht'.to_set.to_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
⊢ LT.lt (α := Submodule k V) (direction (affineSpan k (↑s : Set V))) (direction (affineSpan k (↑t : Set V)))

Tactic:
have dir_lt := AffineSubspace.direction_lt_of_nonempty (k := k) hst <| hs'.to_set.affineSpan k
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
dir_lt : LT.lt (α := Submodule k V) (direction (affineSpan k (↑s : Set V))) (direction (affineSpan k (↑t : Set V)))
⊢ LT.lt (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))

Tactic:
rw [direction_affineSpan, direction_affineSpan,
    ← @Subtype.range_coe _ (s : Set V), ← @Subtype.range_coe _ (t : Set V)] at dir_lt

Premises used: direction_affineSpan, Subtype.range_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
dir_lt :
  LT.lt (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))
⊢ finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V))))) +
      1 <
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1

Tactic:
have finrank_lt := add_lt_add_left (Submodule.finrank_lt_finrank_of_lt dir_lt) 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
dir_lt :
  LT.lt (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))
finrank_lt :
  finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V))))) +
      1 <
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1
⊢ Fintype.card.{u_2} ↥s <
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1

Tactic:
erw [hs.finrank_vectorSpan_add_one] at finrank_lt

Premises used: AffineIndependent.finrank_vectorSpan_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑t : Set V))
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
dir_lt :
  LT.lt (α := Submodule k V)
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑s : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))))
    (vectorSpan k (P := V)
      (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))))
finrank_lt :
  Fintype.card.{u_2} ↥s <
    finrank.{u_1, u_2} k
        ↥(vectorSpan k (P := V)
            (Set.range (ι := { x : V // x ∈ (↑t : Set V) }) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V))))) +
      1
⊢ #s < #t

Tactic:
simpa using finrank_lt.trans_le <| finrank_vectorSpan_range_add_one_le _ _

Premises used: LT.lt.trans_le, finrank_vectorSpan_range_add_one_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sm : Submodule k V
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sm
hle : vectorSpan k (↑(Finset.image p s) : Set P) ≤ sm
hc : #s = finrank.{u_1, u_2} k ↥sm + 1
⊢ vectorSpan k (↑(Finset.image p s) : Set P) = sm

Tactic:
Submodule.eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan_image_finset hc

Premises used: AffineIndependent.finrank_vectorSpan_image_finset, Submodule.eq_of_le_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hi : AffineIndependent k p
sm : Submodule k V
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sm
hle : vectorSpan k (Set.range p) ≤ sm
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥sm + 1
⊢ vectorSpan k (Set.range p) = sm

Tactic:
Submodule.eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan hc

Premises used: AffineIndependent.finrank_vectorSpan, Submodule.eq_of_le_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
rw : 0 < finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ s.Nonempty

Tactic:
rw [← Finset.card_pos, hc]

Premises used: Finset.card_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ 0 < finrank.{u_1, u_2} k ↥sp.direction + 1

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ s.Nonempty

Tactic:
have hn : s.Nonempty := by
    rw [← Finset.card_pos, hc]
    apply Nat.succ_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
hn : s.Nonempty
⊢ affineSpan k (↑(Finset.image p s) : Set P) = sp

Tactic:
eq_of_direction_eq_of_nonempty_of_le ?_ ((hn.image p).to_set.affineSpan k) hle

Premises used: Finset.Nonempty.image, AffineSubspace.eq_of_direction_eq_of_nonempty_of_le, Set.Nonempty.affineSpan, Finset.Nonempty.to_set