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
hi : AffineIndependent k p
n : ℕ
hc : Fintype.card ι = n + 1
rw rw₁ rw₂ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1), finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
rw₃ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) = n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n

Tactic:
classical
  rw [← Finset.card_univ] at hc
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
  exact hi.finrank_vectorSpan_image_finset hc

Premises used: Finset.card_univ, Set.image_univ, Finset.coe_univ, Finset.coe_image
-- 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 ι
inst_5 : Nonempty ι
p : ι → P
hi : AffineIndependent k p
rw rw₁ : 1 ≤ Fintype.card ι
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι

Tactic:
rw [hi.finrank_vectorSpan (tsub_add_cancel_of_le _).symm, tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le, AffineIndependent.finrank_vectorSpan, 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 ι
inst_5 : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ 1 ≤ Fintype.card ι

Tactic:
Fintype.card_pos

Premises used: Fintype.card_pos, Nat.lt
-- 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 ι
inst_5 : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ 1 ≤ Fintype.card ι

Tactic:
exact Fintype.card_pos

Premises used: Fintype.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 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k V + 1
⊢ Eq (α := Submodule k V) (vectorSpan k (Set.range p)) ⊤

Tactic:
Submodule.eq_top_of_finrank_eq <| hi.finrank_vectorSpan hc

Premises used: AffineIndependent.finrank_vectorSpan, Submodule.eq_top_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
s : Finset ι
n : ℕ
hc : #s = n + 1
rw : 0 < n + 1
⊢ (Finset.image p s).Nonempty

Tactic:
rw [Finset.image_nonempty, ← Finset.card_pos, hc]

Premises used: Finset.image_nonempty, 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
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ 0 < n + 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
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ (Finset.image p s).Nonempty

Tactic:
have hn : (s.image p).Nonempty := by
    rw [Finset.image_nonempty, ← 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
s : Finset ι
n : ℕ
hc : #s = n + 1
hn : (Finset.image p s).Nonempty
rcases :
  ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n

Tactic:
rcases hn with ⟨p₁, hp₁⟩
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
rw :
  finrank.{u_1, u_2} k
      ↥(Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)) ≤
    n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n

Tactic:
rw [vectorSpan_eq_span_vsub_finset_right_ne k hp₁]

Premises used: vectorSpan_eq_span_vsub_finset_right_ne
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank.{u_1, u_2} k
      ↥(Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)) ≤
    n

Tactic:
le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) ?_

Premises used: VSub.vsub, finrank_span_finset_le_card, Finset.erase, Finset.image, le_trans
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
refine : Finset.card.{u_2} (α := V) (Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) ≤ n
⊢ finrank.{u_1, u_2} k
      ↥(Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)) ≤
    n

Tactic:
refine le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) ?_

Premises used: VSub.vsub, finrank_span_finset_le_card, Finset.erase, Finset.image, le_trans
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
rw : #(Finset.image p s) ≤ #s
⊢ Finset.card.{u_2} (α := V) (Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) ≤ n

Tactic:
rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁,
    tsub_le_iff_right, ← hc]

Premises used: Finset.card_erase_of_mem, Finset.card_image_of_injective, tsub_le_iff_right, vsub_left_injective
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ #(Finset.image p s) ≤ #s

Tactic:
apply Finset.card_image_le

Premises used: Finset.card_image_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
s : Finset ι
n : ℕ
hc : #s = n + 1
have : (Finset.image p s).Nonempty
have₁ : ∀ (hn : (Finset.image p s).Nonempty), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have₂ : (Finset.image p s).Nonempty
have₃ have₄ :
  ∀ (hn : (Finset.image p s).Nonempty), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have₅ : ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have₆ :
  ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s),
    finrank.{u_1, u_2} k
        ↥(Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)) ≤
      n
have₇ :
  ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s),
    Finset.card.{u_2} (α := V) (Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) ≤ n
have₈ : ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s), #(Finset.image p s) ≤ #s
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n

Tactic:
classical
  have hn : (s.image p).Nonempty := by
    rw [Finset.image_nonempty, ← Finset.card_pos, hc]
    apply Nat.succ_pos
  rcases hn with ⟨p₁, hp₁⟩
  rw [vectorSpan_eq_span_vsub_finset_right_ne k hp₁]
  refine le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) ?_
  rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁,
    tsub_le_iff_right, ← hc]
  apply Finset.card_image_le

Premises used: tsub_le_iff_right, Finset.card_image_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 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n

Tactic:
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ Finset.card.{u_4} (α := ι) Finset.univ = n + 1

Tactic:
rw [← Finset.card_univ] at hc

Premises used: Finset.card_univ
-- 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
n : ℕ
hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n

Tactic:
finrank_vectorSpan_image_finset_le _ _ _ hc

Premises used: finrank_vectorSpan_image_finset_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 : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n

Tactic:
exact finrank_vectorSpan_image_finset_le _ _ _ hc

Premises used: finrank_vectorSpan_image_finset_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 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' Set.univ)) ≤ n
rw₁ : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' (↑Finset.univ : Set ι))) ≤ n
rw₂ rw₃ rw₄ : finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
rw₅ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n

Tactic:
classical
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
  rw [← Finset.card_univ] at hc
  exact finrank_vectorSpan_image_finset_le _ _ _ hc

Premises used: Finset.card_univ, Set.image_univ, finrank_vectorSpan_image_finset_le, Finset.coe_univ, Finset.coe_image
-- 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 ι
inst_5 : Nonempty ι
p : ι → P
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1 ≤ Fintype.card ι

Tactic:
(le_tsub_iff_right <| Nat.succ_le_iff.2 Fintype.card_pos).1 <| finrank_vectorSpan_range_le _ _
    (tsub_add_cancel_of_le <| Nat.succ_le_iff.2 Fintype.card_pos).symm

Premises used: Iff.mpr, tsub_add_cancel_of_le, Iff.mp, Eq.symm, Nat.succ_le_iff, le_tsub_iff_right, Fintype.card_pos, finrank_vectorSpan_range_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 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ Nonempty ι

Tactic:
simp [← Fintype.card_pos_iff, hc]

Premises used: Fintype.card_pos_iff
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ Nonempty ι

Tactic:
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
hn : Nonempty ι
obtain : ∀ (i₁ : ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n

Tactic:
obtain ⟨i₁⟩ := hn
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
rw :
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]

Premises used: Set.finrank, eq_comm, vectorSpan_range_eq_span_range_vsub_right_ne, affineIndependent_iff_linearIndependent_vsub, linearIndependent_iff_card_eq_finrank_span
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
rw :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1) (i₁ : ι),
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
        Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
      finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
⊢ finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n

Tactic:
rw [← Finset.card_univ] at hc

Premises used: Finset.card_univ
-- 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
n : ℕ
hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1
i₁ : ι
rw :
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Finset.card.{u_4} (α := ι) {x : ι | x ≠ i₁} ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
⊢ finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n

Tactic:
rw [Fintype.subtype_card]

Premises used: Fintype.subtype_card
-- 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
n : ℕ
hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1
i₁ : ι
⊢ finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Finset.card.{u_4} (α := ι) {x : ι | x ≠ i₁} ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n

Tactic:
simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]

Premises used: Finset.card_erase_of_mem, Finset.filter_ne'
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
have : Nonempty ι
have₁ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₂ : Nonempty ι
have₃ have₄ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₅ : ∀ (i₁ : ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₆ :
  ∀ (i₁ : ι),
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
        Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
      finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
have₇ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1) (i₁ : ι),
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
        Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
      finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
have₈ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1) (i₁ : ι),
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
        Finset.card.{u_4} (α := ι) {x : ι | x ≠ i₁} ↔
      finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n

Tactic:
classical
  have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]

Premises used: Finset.card_univ, Fintype.subtype_card, Set.finrank, Finset.card_erase_of_mem, eq_comm, Finset.filter_ne', linearIndependent_iff_card_eq_finrank_span
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n ↔ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
⊢ AffineIndependent k p ↔ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))

Tactic:
rw [affineIndependent_iff_finrank_vectorSpan_eq k p hc]

Premises used: affineIndependent_iff_finrank_vectorSpan_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
n : ℕ
hc : Fintype.card ι = n + 1
mp : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n → n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
mpr : n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) → finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n ↔ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))

Tactic:
constructor
-- 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
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))

Tactic:
rfl
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) → finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n

Tactic:
fun hle => le_antisymm (finrank_vectorSpan_range_le k p hc) hle

Premises used: le_antisymm, finrank_vectorSpan_range_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 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) → finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n

Tactic:
exact fun hle => le_antisymm (finrank_vectorSpan_range_le k p hc) hle

Premises used: le_antisymm, finrank_vectorSpan_range_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 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
rw :
  n + 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
rw₁ : n < finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
rw₂ rw₃ :
  ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
⊢ AffineIndependent k p ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n

Tactic:
rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]

Premises used: lt_iff_not_ge, affineIndependent_iff_le_finrank_vectorSpan, Nat.lt_iff_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 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n ↔ ¬AffineIndependent k p

Tactic:
(not_iff_comm.1 (affineIndependent_iff_not_finrank_vectorSpan_le k p hc).symm).symm

Premises used: affineIndependent_iff_not_finrank_vectorSpan_le, Iff.mp, Iff.symm, not_iff_comm