awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
n : ℕ
hc : #s = n + 1
have have₁ have₂ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₃ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₄ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (hn : (Finset.image p s).Nonempty),
    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
have have₅ : ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
  (hc' : #(Finset.image p s) = n + 1) (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s),
  finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
Tactic: classical
  have hi' := hi.range.mono (Set.image_subset_range p ↑s)
  have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
  have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
  rcases hn with ⟨p₁, hp₁⟩
  have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
  rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
  have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
  rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, 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 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
have have₁ have₂ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₃ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₄ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (hn : (Finset.image p s).Nonempty),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₅ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (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
have have₆ : ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
  (hc' : #(Finset.image p s) = n + 1) (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s) (hp₁' : p₁ ∈ p '' (↑s : Set ι)),
  finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
Tactic: classical
  have hi' := hi.range.mono (Set.image_subset_range p ↑s)
  have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
  have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
  rcases hn with ⟨p₁, hp₁⟩
  have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
  rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
  have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
  rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, 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 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
have have₁ have₂ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₃ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₄ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (hn : (Finset.image p s).Nonempty),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₅ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₆ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s) (hp₁' : p₁ ∈ p '' (↑s : Set ι)),
    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
have have₇ : ∀ (hc' : #(Finset.image p s) = n + 1) (p₁ : P)
  (hi' :
    LinearIndependent k (M := V)
      fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦
      (↑v : V))
  (hp₁ : p₁ ∈ Finset.image p s) (hp₁' : p₁ ∈ p '' (↑s : Set ι)),
  finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
Tactic: classical
  have hi' := hi.range.mono (Set.image_subset_range p ↑s)
  have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
  have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
  rcases hn with ⟨p₁, hp₁⟩
  have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
  rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
  have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
  rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, 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 : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have hc₁ : Finset.card.{u_4} (α := ι) Finset.univ = n + 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
n : ℕ
hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have rw : finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) = n
Tactic: rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have rw : ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1), 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
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
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
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have 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
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
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 ι
inst_5 : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι
have rw : 1 ≤ Fintype.card ι
Tactic: rw [hi.finrank_vectorSpan (tsub_add_cancel_of_le _).symm, tsub_add_cancel_of_le]
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ (Finset.image p s).Nonempty
have rw : 0 < n + 1
Tactic: rw [Finset.image_nonempty, ← 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
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have hn : (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
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
hn : (Finset.image p s).Nonempty
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
Tactic: rcases hn with ⟨p₁, hp₁⟩
Cleared hypotheses: 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 : 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 ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have 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
Tactic: rw [vectorSpan_eq_span_vsub_finset_right_ne k hp₁]
-- 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
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
have refine : Finset.card.{u_2} (α := V) (Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) ≤ n
Tactic: refine le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) ?_
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
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 rw : #(Finset.image p s) ≤ #s
Tactic: rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁,
    tsub_le_iff_right, ← 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 : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have have : (Finset.image p s).Nonempty
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
-- 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
s : Finset ι
n : ℕ
hc : #s = n + 1
have : (Finset.image p s).Nonempty
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have have₁ : ∀ (hn : (Finset.image p s).Nonempty), 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
-- 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
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
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have have₅ : ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p 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
-- 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
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
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have 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
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
-- 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
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
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have 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
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
-- 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
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
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) ≤ n
have have₈ : ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s), #(Finset.image p s) ≤ #s
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
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw : finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
Tactic: rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
have hc₁ : Finset.card.{u_4} (α := ι) Finset.univ = n + 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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' Set.univ)) ≤ 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
-- 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
n : ℕ
hc : Fintype.card ι = n + 1
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' Set.univ)) ≤ n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw₁ : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' (↑Finset.univ : Set ι))) ≤ 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