awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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)))
⊢ #s ≤ #t
have 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)))))
Tactic: rw [AffineSubspace.affineSpan_coe, direction_affineSpan, direction_affineSpan,
    ← @Subtype.range_coe _ (s : Set V), ← @Subtype.range_coe _ (t : Set V)] at direction_le
Cleared hypotheses: direction_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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)))))
⊢ #s ≤ #t
have 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
Tactic: have finrank_le := add_le_add_left (Submodule.finrank_mono direction_le) 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
⊢ #s ≤ #t
have 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
Tactic: erw [hs.finrank_vectorSpan_add_one] at finrank_le
Cleared hypotheses: finrank_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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))
⊢ #s < #t
have 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
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs, hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ #s < #t
have inr : ∀ (hs' : s.Nonempty), #s < #t
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ #s < #t
have inr : ∀ (hst : LT.lt (α := AffineSubspace k V) (affineSpan k (↑s : Set V)) (affineSpan k (↑∅ : Set V))),
  #s < card.{u_2} (α := V) ∅
Tactic: obtain rfl | ht' := t.eq_empty_or_nonempty
Cleared hypotheses: t, hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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) ∅
⊢ #s < #t
have inr₁ : ∀ (ht' : t.Nonempty), #s < #t
Tactic: obtain rfl | ht' := t.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
⊢ #s < #t
have this : Nonempty.{u_2 + 1} ↥s
Tactic: have := hs'.to_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
⊢ #s < #t
have this₁ : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
Tactic: have := ht'.to_set.to_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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)
⊢ #s < #t
have dir_lt : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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)))
⊢ #s < #t
have 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)))))
Tactic: rw [direction_affineSpan, direction_affineSpan,
    ← @Subtype.range_coe _ (s : Set V), ← @Subtype.range_coe _ (t : Set V)] at dir_lt
Cleared hypotheses: dir_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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)))))
⊢ #s < #t
have 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
Tactic: have finrank_lt := add_lt_add_left (Submodule.finrank_lt_finrank_of_lt dir_lt) 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
⊢ #s < #t
have 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
Tactic: erw [hs.finrank_vectorSpan_add_one] at finrank_lt
Cleared hypotheses: finrank_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
have rw : 0 < finrank.{u_1, u_2} k ↥sp.direction + 1
Tactic: rw [← Finset.card_pos, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
⊢ affineSpan k (↑(Finset.image p s) : Set P) = sp
have hn : s.Nonempty
Tactic: have hn : s.Nonempty := by
    rw [← Finset.card_pos, hc]
    apply Nat.succ_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
have refine : direction (affineSpan k (↑(Finset.image p s) : Set P)) = sp.direction
Tactic: refine eq_of_direction_eq_of_nonempty_of_le ?_ ((hn.image p).to_set.affineSpan k) hle
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
⊢ direction (affineSpan k (↑(Finset.image p s) : Set P)) = sp.direction
have hd : direction (affineSpan k (↑(Finset.image p s) : Set P)) ≤ sp.direction
Tactic: have hd := direction_le hle
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hd : direction (affineSpan k (↑(Finset.image p s) : Set P)) ≤ sp.direction
⊢ direction (affineSpan k (↑(Finset.image p s) : Set P)) = sp.direction
have rw : ∀ (hd : vectorSpan k (↑(Finset.image p s) : Set P) ≤ sp.direction),
  vectorSpan k (↑(Finset.image p s) : Set P) = sp.direction
Tactic: rw [direction_affineSpan] at hd ⊢
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ affineSpan k (Set.range p) = sp
have hc₁ : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1
Tactic: rw [← Finset.card_univ] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ affineSpan k (Set.range p) = sp
have rw : ∀ (hle : affineSpan k (↑(Finset.image p Finset.univ) : Set P) ≤ sp)
  (hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1),
  affineSpan k (↑(Finset.image p Finset.univ) : Set P) = sp
Tactic: rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢
Cleared hypotheses: hle, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ affineSpan k (Set.range p) = sp
have rw : ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1),
  affineSpan k (Set.range p) = sp
Tactic: classical
  rw [← Finset.card_univ] at hc
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢
  exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥sp.direction + 1
rw rw₁ rw₂ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1),
    affineSpan k (Set.range p) = sp
⊢ affineSpan k (Set.range p) = sp
have rw₃ : ∀ (hle : affineSpan k (↑(Finset.image p Finset.univ) : Set P) ≤ sp)
  (hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1),
  affineSpan k (↑(Finset.image p Finset.univ) : Set P) = sp
Tactic: classical
  rw [← Finset.card_univ] at hc
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢
  exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc
Cleared hypotheses: hle, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤ ↔ Fintype.card ι = finrank k V + 1
have mp : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤ → Fintype.card ι = finrank k V + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
mp : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤ → Fintype.card ι = finrank k V + 1
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤ ↔ Fintype.card ι = finrank k V + 1
have mpr : Fintype.card ι = finrank k V + 1 → Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
n : ℕ := Fintype.card ι - 1
⊢ Fintype.card ι = finrank k V + 1
have hn : Fintype.card ι = n + 1
Tactic: have hn : Fintype.card ι = n + 1 :=
      (Nat.succ_pred_eq_of_pos (card_pos_of_affineSpan_eq_top k V P h_tot)).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
⊢ Fintype.card ι = finrank k V + 1
have mp : n + 1 = finrank k V + 1
Tactic: rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
      ← hi.finrank_vectorSpan hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
mp : n + 1 = finrank k V + 1
⊢ Fintype.card ι = finrank k V + 1
have mp₁ : n + 1 = finrank.{u_1, u_2} k ↥⊤ + 1
Tactic: rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
      ← hi.finrank_vectorSpan hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
mp : n + 1 = finrank k V + 1
mp₁ : n + 1 = finrank.{u_1, u_2} k ↥⊤ + 1
⊢ Fintype.card ι = finrank k V + 1
have mp₂ : n + 1 = finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
Tactic: rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
      ← hi.finrank_vectorSpan hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
mp : n + 1 = finrank k V + 1
mp₁ : n + 1 = finrank.{u_1, u_2} k ↥⊤ + 1
mp₂ : n + 1 = finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
⊢ Fintype.card ι = finrank k V + 1
have mp₃ : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1 = finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
Tactic: rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
      ← hi.finrank_vectorSpan hn]