awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p) ↔ AffineIndependent k p

Tactic:
⟨AffineIndependent.of_comp f, fun hai => AffineIndependent.map' hai f hf⟩

Premises used: AffineIndependent.map', Iff.intro, AffineIndependent.of_comp
-- 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
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
e : P ≃ᵃ[k] P₂
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑e : (a : P) → P₂) ∘ p) ↔ AffineIndependent k p

Tactic:
e.toAffineMap.affineIndependent_iff e.toEquiv.injective

Premises used: AffineEquiv.toAffineMap, AffineEquiv.toEquiv, Equiv.injective, AffineMap.affineIndependent_iff
-- 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
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
⊢ Eq (α := { x : P // x ∈ s } → P₂) ((⇑e : (a : P) → P₂) ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s))
    (comp (β := { x : P₂ // Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x })
      (Subtype.val (p := fun (x : P₂) ↦ Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x))
      (⇑((↑e : P ≃ P₂).image s) : (a : (↑s : Type u_3)) → (↑((⇑(↑e : P ≃ P₂) : (a : P) → P₂) '' s) : Type u_6)))

Tactic:
have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl
-- 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
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
this :
  Eq (α := { x : P // x ∈ s } → P₂) ((⇑e : (a : P) → P₂) ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s))
    (comp (β := { x : P₂ // Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x })
      (Subtype.val (p := fun (x : P₂) ↦ Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x))
      (⇑((↑e : P ≃ P₂).image s) : (a : (↑s : Type u_3)) → (↑((⇑(↑e : P ≃ P₂) : (a : P) → P₂) '' s) : Type u_6)))
⊢ AffineIndependent.{u_1, u_5, u_6, u_6} k (P := P₂) (ι :=
      { x : P₂ // Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x })
      (Subtype.val (p := fun (x : P₂) ↦ Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x)) ↔
    AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
simp [← e.affineIndependent_iff, this, affineIndependent_equiv]

Premises used: affineIndependent_equiv, AffineEquiv.affineIndependent_iff
-- 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'
⊢ Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) (affineSpan k (p '' (s₁ ∩ s₂)))

Tactic:
ext p'
-- 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 ι
p' : P
h :
  ((∃ (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
⊢ 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'

Tactic:
simp_rw [AffineSubspace.mem_inf_iff, Set.image_eq_range, mem_affineSpan_iff_eq_affineCombination,
    ← Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype]

Premises used: mem_affineSpan_iff_eq_affineCombination, Set.image_eq_range, Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype, AffineSubspace.mem_inf_iff
-- 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 ι
p' : P
h :
  ((∃ (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₁ :
  (∃ (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
⊢ ((∃ (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

Tactic:
constructor
-- 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 ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
h :
  ∀
    (ha :
      ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
          Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
            Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
                ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
              (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2)
    (s₁ s₂ : Set ι) (fs₁ : Finset ι) (hfs₁ : (↑fs₁ : Set ι) ⊆ s₁) (w₁ : ι → k)
    (hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1) (fs₂ : Finset ι) (hfs₂ : (↑fs₂ : Set ι) ⊆ s₂) (w₂ : ι → k)
    (hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1)
    (hw₁₂ :
      Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
        ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)),
    ∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
        ∃ (w : ι → k),
          Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
            Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
              ((affineCombination k fs p : (a : ι → k) → P) w : P)
⊢ ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k fs p : (a : ι → k) → P) w : P)

Tactic:
rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha

Premises used: affineIndependent_iff_indicator_eq_of_affineCombination_eq
-- 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 :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
⊢ (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂

Tactic:
replace ha := ha fs₁ fs₂ w₁ w₂ hw₁ hw₂ hw₁₂
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
⊢ (↑(fs₁ ∩ fs₂) : Set ι) ⊆ s₁ ∩ s₂

Tactic:
grind
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁ ∩ fs₂, w₁ i) 1
h₁ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k (fs₁ ∩ fs₂) p : (a : ι → k) → P) w₁ : P)
⊢ ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k fs p : (a : ι → k) → P) w : P)

Tactic:
refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
h : HAdd.hAdd (α := k) (∑ x ∈ fs₁ ∩ fs₂, w₁ x) (∑ x ∈ fs₁ \ fs₂, w₁ x) = ∑ i ∈ fs₁ ∩ fs₂, w₁ i
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁ ∩ fs₂, w₁ i) 1

Tactic:
rw [← hw₁, ← fs₁.sum_inter_add_sum_diff fs₂, eq_comm]

Premises used: Finset.sum_inter_add_sum_diff, eq_comm
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
⊢ HAdd.hAdd (α := k) (∑ x ∈ fs₁ ∩ fs₂, w₁ x) 0 = ∑ x ∈ fs₁ ∩ fs₂, w₁ x

Tactic:
add_zero _

Premises used: add_zero
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
h : Eq.{u_1 + 1} (α := k) (∑ x ∈ fs₁ \ fs₂, w₁ x) 0
⊢ HAdd.hAdd (α := k) (∑ x ∈ fs₁ ∩ fs₂, w₁ x) (∑ x ∈ fs₁ \ fs₂, w₁ x) = ∑ i ∈ fs₁ ∩ fs₂, w₁ i

Tactic:
convert! add_zero _

Premises used: add_zero
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ fs₁ \ fs₂, w₁ x) 0

Tactic:
Finset.sum_eq_zero ?_

Premises used: Finset.sum_eq_zero
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
h : ∀ x ∈ fs₁ \ fs₂, w₁ x = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ fs₁ \ fs₂, w₁ x) 0

Tactic:
refine Finset.sum_eq_zero ?_

Premises used: Finset.sum_eq_zero
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁ \ fs₂
⊢ i ∈ (↑fs₁ : Set ι)

Tactic:
grind
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁ \ fs₂
⊢ i ∉ (↑fs₂ : Set ι)

Tactic:
grind
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁ \ fs₂
h : (↑fs₁ : Set ι).indicator w₁ i = 0
h₁ : (↑fs₂ : Set ι).indicator w₂ i = 0
h₂ h₃ : Eq.{u_1 + 1} (α := k) 0 0
⊢ w₁ i = 0

Tactic:
rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]

Premises used: Set.indicator_of_mem, Set.indicator_of_notMem
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₁ p : (a : ι → k) → P) ((↑(fs₁ ∩ fs₂) : Set ι).indicator w₁) : P)
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k (fs₁ ∩ fs₂) p : (a : ι → k) → P) w₁ : P)

Tactic:
rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]

Premises used: Finset.affineCombination_indicator_subset, Finset.inter_subset_left
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₁ p : (a : ι → k) → P) ((↑(fs₁ ∩ fs₂) : Set ι).indicator w₁) : P)

Tactic:
affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)

Premises used: Finset.affineCombination_congr, rfl
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
h : ∀ i ∈ fs₁, w₁ i = (↑(fs₁ ∩ fs₂) : Set ι).indicator w₁ i
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₁ p : (a : ι → k) → P) ((↑(fs₁ ∩ fs₂) : Set ι).indicator w₁) : P)

Tactic:
refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)

Premises used: Finset.affineCombination_congr, rfl
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁
⊢ i ∈ (↑fs₁ : Set ι)

Tactic:
simpa using hi
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁
h : w₁ i = if i ∈ (↑fs₂ : Set ι) then w₁ i else 0
⊢ w₁ i = (↑(fs₁ ∩ fs₂) : Set ι).indicator w₁ i

Tactic:
rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]

Premises used: Set.indicator_apply, Set.indicator_of_mem, Set.indicator_indicator, Finset.coe_inter
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁
h : i ∉ fs₂ → w₁ i = 0
⊢ w₁ i = if i ∈ (↑fs₂ : Set ι) then w₁ i else 0

Tactic:
simp only [mem_coe, left_eq_ite_iff]

Premises used: left_eq_ite_iff, Finset.mem_coe