-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h :
  ∀ (p' : P),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) p' ↔
      Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s₁ ∩ s₂))) p'
h₁ :
  ∀ (p' : P),
    ((∃ (fs : Finset ι),
          (↑fs : Set ι) ⊆ s₁ ∧
            ∃ (w : ι → k),
              Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
        ∃ (fs : Finset ι),
          (↑fs : Set ι) ⊆ s₂ ∧
            ∃ (w : ι → k),
              Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ↔
      ∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
          ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
h₂ :
  ∀ (p' : P),
    ((∃ (fs : Finset ι),
          (↑fs : Set ι) ⊆ s₁ ∧
            ∃ (w : ι → k),
              Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
        ∃ (fs : Finset ι),
          (↑fs : Set ι) ⊆ s₂ ∧
            ∃ (w : ι → k),
              Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) →
      ∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
          ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
h₃ h₄ :
  ∀ (p' : P),
    (∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) →
      (∃ (fs : Finset ι),
          (↑fs : Set ι) ⊆ s₁ ∧
            ∃ (w : ι → k),
              Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
        ∃ (fs : Finset ι),
          (↑fs : Set ι) ⊆ s₂ ∧
            ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
⊢ Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) (affineSpan k (p '' (s₁ ∩ s₂)))

Tactic:
classical
  ext p'
  simp_rw [AffineSubspace.mem_inf_iff, Set.image_eq_range, mem_affineSpan_iff_eq_affineCombination,
    ← Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype]
  constructor
  · rintro ⟨⟨fs₁, hfs₁, w₁, hw₁, rfl⟩, ⟨fs₂, hfs₂, w₂, hw₂, hw₁₂⟩⟩
    rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
    replace ha := ha fs₁ fs₂ w₁ w₂ hw₁ hw₂ hw₁₂
    refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
    · rw [← hw₁, ← fs₁.sum_inter_add_sum_diff fs₂, eq_comm]
      convert! add_zero _
      refine Finset.sum_eq_zero ?_
      intro i hi
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
    · rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]
      refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)
      intro i hi
      rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]
      simp only [mem_coe, left_eq_ite_iff]
      intro hi₂
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]
      simp [hi₂]
  · grind

Premises used: Set.indicator_apply, Finset.affineCombination_congr, Finset.sum_eq_zero, mem_affineSpan_iff_eq_affineCombination, affineIndependent_iff_indicator_eq_of_affineCombination_eq, left_eq_ite_iff, Set.image_eq_range, eq_comm, Set.indicator_of_mem, Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype, Set.indicator_indicator, AffineSubspace.mem_inf_iff, Set.indicator_of_notMem, add_zero, Finset.coe_inter, Finset.mem_coe, rfl