-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one [Fintype ι] {p : ι → P}
    (hi : AffineIndependent k p) {sp : AffineSubspace k P} [FiniteDimensional k sp.direction]
    (hle : affineSpan k (Set.range p) ≤ sp) (hc : Fintype.card ι = finrank k sp.direction + 1) :
    affineSpan k (Set.range p) = sp

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : #Finset.univ = finrank k ↥sp.direction + 1
⊢ affineSpan k (Set.range p) = sp

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

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p Finset.univ) ≤ sp
hc : #Finset.univ = finrank k ↥sp.direction + 1
⊢ affineSpan k ↑(Finset.image p Finset.univ) = sp

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank k ↥sp.direction + 1
⊢ affineSpan k (Set.range p) = sp

Tactic:
rw [← Finset.card_univ] at hc

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : #Finset.univ = finrank k ↥sp.direction + 1
⊢ affineSpan k (Set.range p) = sp

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank 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

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p Finset.univ) ≤ sp
hc : #Finset.univ = finrank k ↥sp.direction + 1
⊢ affineSpan k ↑(Finset.image p Finset.univ) = sp

Tactic:
exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc

Result:
no goals