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
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : s.Finite
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))

Tactic:
(direction_affineSpan k s).symm ▸ finiteDimensional_vectorSpan_of_finite k h

Premises used: direction_affineSpan, finiteDimensional_vectorSpan_of_finite, Eq.rec, 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
p : P
rw : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) {p})
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (P := P) (affineSpan k {p}))

Tactic:
rw [direction_affineSpan]

Premises used: direction_affineSpan
-- 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
p : P
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) {p})

Tactic:
infer_instance
-- 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 : Finite ι
p : ι → P
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (Set.range p)))

Tactic:
finiteDimensional_direction_affineSpan_of_finite k (Set.finite_range _)

Premises used: finiteDimensional_direction_affineSpan_of_finite, Set.finite_range
-- 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 : Finite ι
p : ι → P
s : Set ι
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (p '' s)))

Tactic:
finiteDimensional_direction_affineSpan_of_finite k (Set.toFinite _)

Premises used: finiteDimensional_direction_affineSpan_of_finite, Set.toFinite
-- 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
p : ι → P
hi : AffineIndependent k p
⊢ Nontrivial ι

Tactic:
nontriviality ι
-- 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
p : ι → P
hi : AffineIndependent k p
h : Nontrivial ι
inhabit : ∀ (inhabited_h : Inhabited ι), Finite ι
⊢ Finite ι

Tactic:
inhabit ι
-- 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
p : ι → P
hi : AffineIndependent k p
h : Nontrivial ι
inhabited_h : Inhabited ι
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ default }) ↦ p (↑i : ι) -ᵥ p default

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k p default] at hi

Premises used: Inhabited.default, affineIndependent_iff_linearIndependent_vsub
-- 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
p : ι → P
h : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ default }) ↦ p (↑i : ι) -ᵥ p default
this : IsNoetherian k V := ⋯
⊢ Finite ι

Tactic:
(Set.finite_singleton default).finite_of_compl (Set.finite_coe_iff.1 hi.finite_of_isNoetherian)

Premises used: Inhabited.default, Set.Finite.finite_of_compl, Set.finite_coe_iff, Iff.mp, LinearIndependent.finite_of_isNoetherian, Set.finite_singleton
-- 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
p : ι → P
h : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ default }) ↦ p (↑i : ι) -ᵥ p default
this : IsNoetherian k V := ⋯
⊢ Finite ι

Tactic:
exact
    (Set.finite_singleton default).finite_of_compl (Set.finite_coe_iff.1 hi.finite_of_isNoetherian)

Premises used: Inhabited.default, Set.Finite.finite_of_compl, Set.finite_coe_iff, Iff.mp, LinearIndependent.finite_of_isNoetherian, Set.finite_singleton
-- 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
s : Set ι
f : (↑s : Type u_4) → P
hi : AffineIndependent k f
⊢ s.Finite

Tactic:
@Set.toFinite _ s (finite_of_fin_dim_affineIndependent k hi)

Premises used: Set.toFinite
-- 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
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
inl :
  ∀ [FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)],
    FiniteDimensional.{u_1, u_2} k ↥(⊥ ⊔ s₂).direction
inr : ∀ (p₁ : P) (hp₁ : p₁ ∈ (↑s₁ : Set P)), FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction

Tactic:
rcases eq_bot_or_nonempty s₁ with rfl | ⟨p₁, hp₁⟩

Premises used: AffineSubspace.eq_bot_or_nonempty, 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
s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)
inl inl₁ inl₂ inl₃ : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
⊢ FiniteDimensional.{u_1, u_2} k ↥(⊥ ⊔ s₂).direction

Tactic:
rwa [bot_sup_eq]

Premises used: bot_sup_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
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
inr :
  ∀ [FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)],
    FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ ⊥).direction
inr₁ : ∀ (p₂ : P) (hp₂ : p₂ ∈ (↑s₂ : Set P)), FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction

Tactic:
rcases eq_bot_or_nonempty s₂ with rfl | ⟨p₂, hp₂⟩

Premises used: AffineSubspace.eq_bot_or_nonempty, 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
s₁ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
inst_5 : FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)
inr inr₁ inr₂ inr₃ : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ ⊥).direction

Tactic:
rwa [sup_bot_eq]

Premises used: sup_bot_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
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
inr : FiniteDimensional.{u_1, u_2} k ↥(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁))
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction

Tactic:
rw [AffineSubspace.direction_sup hp₁ hp₂]

Premises used: AffineSubspace.direction_sup
-- 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
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁))

Tactic:
infer_instance
-- 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
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : AffineSubspace k P
inst_7 : FiniteDimensional.{u_1, u_2} k ↥s.direction
f : P →ᵃ[k] P₂
rw : FiniteDimensional.{u_1, u_5} k ↥(Submodule.map f.linear s.direction)
⊢ FiniteDimensional.{u_1, u_5} k ↥(map f s).direction

Tactic:
rw [map_direction]

Premises used: AffineSubspace.map_direction
-- 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
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : AffineSubspace k P
inst_7 : FiniteDimensional.{u_1, u_2} k ↥s.direction
f : P →ᵃ[k] P₂
⊢ FiniteDimensional.{u_1, u_5} k ↥(Submodule.map f.linear s.direction)

Tactic:
infer_instance
-- 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 ι
n : ℕ
hc : #s = n + 1
⊢ AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)

Tactic:
have hi' := hi.range.mono (Set.image_subset_range p ↑s)
-- 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 ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
rwa rwa₁ rwa₂ rwa₃ : #s = n + 1
⊢ #(Finset.image p s) = n + 1

Tactic:
rwa [s.card_image_of_injective hi.injective]

Premises used: AffineIndependent.injective, Finset.card_image_of_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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
⊢ #(Finset.image p s) = n + 1

Tactic:
have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
hc' : #(Finset.image p s) = n + 1
⊢ (Finset.image p s).Nonempty

Tactic:
simp [hc', ← Finset.card_pos]

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 ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
hc' : #(Finset.image p s) = n + 1
⊢ (Finset.image p s).Nonempty

Tactic:
have hn : (s.image p).Nonempty := by simp [hc', ← 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 ι
n : ℕ
hc : #s = n + 1
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
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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
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
⊢ p₁ ∈ p '' (↑s : Set ι)

Tactic:
simpa using 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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
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
⊢ p₁ ∈ p '' (↑s : Set ι)

Tactic:
have hp₁' : p₁ ∈ p '' s := by simpa using 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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
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 ι)
⊢ 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)

Tactic:
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'

Premises used: Finset.sdiff_singleton_eq_erase, Finset.coe_singleton, affineIndependent_set_iff_linearIndependent_vsub, Finset.coe_sdiff, 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 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
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 ι)
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)
⊢ p₁ ∈ Finset.image p s

Tactic:
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'

Premises used: Finset.sdiff_singleton_eq_erase, Finset.coe_singleton, affineIndependent_set_iff_linearIndependent_vsub, Finset.coe_sdiff, 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 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
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 ι)
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
⊢ p₁ ∈ p '' (↑s : Set ι)

Tactic:
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'

Premises used: Finset.sdiff_singleton_eq_erase, Finset.coe_singleton, affineIndependent_set_iff_linearIndependent_vsub, Finset.coe_sdiff, 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 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
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 ι)
rw : #(Finset.image p s) - 1 = n
⊢ Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n

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

Premises used: Finset.card_erase_of_mem, Finset.card_image_of_injective, 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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
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 ι)
⊢ #(Finset.image p s) - 1 = n

Tactic:
Nat.pred_eq_of_eq_succ hc'

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

Tactic:
exact Nat.pred_eq_of_eq_succ hc'

Premises used: Nat.pred_eq_of_eq_succ
-- 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 ι
n : ℕ
hc : #s = n + 1
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 ι)
⊢ Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n

Tactic:
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'
-- 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 ι
n : ℕ
hc_1 : #s = n + 1
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 ι)
hc : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
rwa :
  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
rwa₁ : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
rwa₂ : LinearIndepOn k id (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)
rwa₃ : n = n
rwa₄ : LinearIndepOn k id (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)
rwa₅ : n = n
rwa₆ rwa₇ rwa₈ : LinearIndepOn k id (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n

Tactic:
rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]

Premises used: finrank_span_finset_eq_card, 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 : Fintype ι
p : ι → P
hi : AffineIndependent k 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
hi : AffineIndependent k p
n : ℕ
hc : Finset.card.{u_4} (α := ι) Finset.univ = 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
hi : AffineIndependent k 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:
hi.finrank_vectorSpan_image_finset hc

Premises used: AffineIndependent.finrank_vectorSpan_image_finset
-- 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 : 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 hi.finrank_vectorSpan_image_finset hc

Premises used: AffineIndependent.finrank_vectorSpan_image_finset