-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) {s1 s2 : Set ι} {p0 : P} (hp0s1 : p0 ∈ affineSpan k (p '' s1))
    (hp0s2 : p0 ∈ affineSpan k (p '' s2)) : ∃ i : ι, i ∈ s1 ∩ s2

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
replace ha := ha fs1 fs2 w1 w2 hw1 hw2 (hp0s1 ▸ hp0s2)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
ha : (↑fs1).indicator w1 = (↑fs2).indicator w2
⊢ ∃ i, i ∈ s1 ∩ s2

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s1 : p0 ∈ affineSpan k (p '' s1)
hp0s2 : p0 ∈ affineSpan k (p '' s2)
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
rw [Set.image_eq_range] at hp0s1 hp0s2

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s1 : p0 ∈ affineSpan k (Set.range fun x => p ↑x)
hp0s2 : p0 ∈ affineSpan k (Set.range fun x => p ↑x)
⊢ ∃ i, i ∈ s1 ∩ s2

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s1 : ∃ fs, ↑fs ⊆ s1 ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w
hp0s2 : ∃ fs, ↑fs ⊆ s2 ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
rcases hp0s1 with ⟨fs1, hfs1, w1, hw1, hp0s1⟩

Result:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s2 : ∃ fs, ↑fs ⊆ s2 ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
⊢ ∃ i, i ∈ s1 ∩ s2

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
ha : (↑fs1).indicator w1 = (↑fs2).indicator w2
hnz : ∑ i ∈ fs1, w1 i ≠ 0
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
rcases Finset.exists_ne_zero_of_sum_ne_zero hnz with ⟨i, hifs1, hinz⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
ha : (↑fs1).indicator w1 = (↑fs2).indicator w2
hnz : ∑ i ∈ fs1, w1 i ≠ 0
i : ι
hifs1 : i ∈ fs1
hinz : w1 i ≠ 0
⊢ ∃ i, i ∈ s1 ∩ s2

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
ha : (↑fs1).indicator w1 = (↑fs2).indicator w2
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
have hnz : ∑ i ∈ fs1, w1 i ≠ 0 := hw1.symm ▸ one_ne_zero

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
ha : (↑fs1).indicator w1 = (↑fs2).indicator w2
hnz : ∑ i ∈ fs1, w1 i ≠ 0
⊢ ∃ i, i ∈ s1 ∩ s2

Proof state:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
ha : (↑fs1).indicator w1 = (↑fs2).indicator w2
hnz : ∑ i ∈ fs1, w1 i ≠ 0
i : ι
hifs1 : i ∈ fs1
hinz : (↑fs2).indicator w2 i ≠ 0
⊢ i ∈ s2

Tactic:
exact hfs2 (Set.mem_of_indicator_ne_zero hinz)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s1 s2 : Set ι
p0 : P
fs1 : Finset ι
hfs1 : ↑fs1 ⊆ s1
w1 : ι → k
hw1 : ∑ i ∈ fs1, w1 i = 1
hp0s1 : p0 = (affineCombination k fs1 p) w1
fs2 : Finset ι
hfs2 : ↑fs2 ⊆ s2
w2 : ι → k
hw2 : ∑ i ∈ fs2, w2 i = 1
hp0s2 : p0 = (affineCombination k fs2 p) w2
⊢ ∃ i, i ∈ s1 ∩ s2