-- 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.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 : (↑fs2).indicator w2 i ≠ 0
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
use i, hfs1 hifs1

Result:
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

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 (Set.range fun x => p ↑x)
hp0s2 : p0 ∈ affineSpan k (Set.range fun x => p ↑x)
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
rw [mem_affineSpan_iff_eq_affineCombination, ←
  Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype] 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 : ∃ 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

Proof state:
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

Tactic:
rcases hp0s2 with ⟨fs2, hfs2, w2, hw2, 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
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

Proof state:
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

Tactic:
simp_rw [← Set.indicator_of_mem (Finset.mem_coe.2 hifs1) w1, ha] at 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 : (↑fs2).indicator w2 i ≠ 0
⊢ ∃ i, i ∈ s1 ∩ s2