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

Tactic:
simpa [hs] using this
-- 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
p : ι → P
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
hi : (↑s : Set ι).indicator w₁ = (↑s : Set ι).indicator w₂
i : ι
hs : i ∈ s
suffices : (↑s : Set ι).indicator w₁ i = (↑s : Set ι).indicator w₂ i
⊢ w₁ i = w₂ i

Tactic:
suffices Set.indicator s w₁ i = Set.indicator s w₂ i by simpa [hs] using this
-- 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
p : ι → P
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
hi : (↑s : Set ι).indicator w₁ = (↑s : Set ι).indicator w₂
i : ι
hs : i ∈ s
⊢ (↑s : Set ι).indicator w₁ i = (↑s : Set ι).indicator w₂ i

Tactic:
simp [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
ha : AffineIndependent k p
i j : ι
hij : p i = p j
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha

Premises used: affineIndependent_iff_linearIndependent_vsub
-- 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
i j : ι
hij : p i = p j
ha₁ : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
⊢ p i = p j

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha

Premises used: affineIndependent_iff_linearIndependent_vsub
-- 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
i j : ι
ha : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
hij : p i = p j
by_contra : ∀ (hij' : ¬i = j), False
⊢ i = j

Tactic:
by_contra hij'
-- 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
i j : ι
ha : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ False

Tactic:
ha.ne_zero ⟨i, hij'⟩ (vsub_eq_zero_iff_eq.mpr ?_)

Premises used: Iff.mpr, LinearIndependent.ne_zero, vsub_eq_zero_iff_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
i j : ι
ha : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
hij : p i = p j
hij' : ¬i = j
refine : p (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ j) i hij') : ι) = p j
⊢ False

Tactic:
refine ha.ne_zero ⟨i, hij'⟩ (vsub_eq_zero_iff_eq.mpr ?_)

Premises used: Iff.mpr, LinearIndependent.ne_zero, vsub_eq_zero_iff_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
i j : ι
ha : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ p (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ j) i hij') : ι) = p j

Tactic:
simp_all only [ne_eq]

Premises used: ne_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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
i2 : ι2
⊢ ∃ (i : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)

Tactic:
have h : ∃ i : ι2, f i = f i2 := ⟨i2, 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
i2 : ι2
h : ∃ (i : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)
⊢ h.choose (p := fun (i : ι2) ↦ Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)) = i2

Tactic:
have hs : h.choose = i2 := f.injective h.choose_spec
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs_1 : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
i2 : ι2
h : ∃ (i : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)
hs : h.choose (p := fun (i : ι2) ↦ Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)) = i2
simp_rw :
  (if h : ∃ (i2_1 : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i2_1 : ι) ((f : (a : ι2) → ι) i2 : ι) then
      w
        (h.choose (p := fun (i2_1 : ι2) ↦
          Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i2_1 : ι) ((f : (a : ι2) → ι) i2 : ι)))
    else 0) =
    w i2
simp_rw₁ :
  w
      (h.choose (p := fun (i2_1 : ι2) ↦
        Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i2_1 : ι) ((f : (a : ι2) → ι) i2 : ι))) =
    w i2
⊢ w' ((f : (a : ι2) → ι) i2) = w i2

Tactic:
simp_rw [w', dif_pos h, hs]

Premises used: dif_pos
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
⊢ ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2

Tactic:
have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ fs, w' ((f : (a : ι2) → ι) x)) (∑ i ∈ fs, w i)
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0

Tactic:
rw [← hw, Finset.sum_map]

Premises used: Finset.sum_map
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ fs, w' ((f : (a : ι2) → ι) x)) (∑ i ∈ fs, w i)

Tactic:
simp [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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0

Tactic:
have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
rw :
  Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) (w' ∘ (⇑f : (a : ι2) → ι)) : V)
    ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V)
⊢ Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)

Tactic:
rw [← hs, Finset.weightedVSub_map]

Premises used: Finset.weightedVSub_map
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
h : ∀ (i : ι2), (w' ∘ (⇑f : (a : ι2) → ι)) i = w i
⊢ Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) (w' ∘ (⇑f : (a : ι2) → ι)) : V)
    ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V)

Tactic:
congr with i
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
i : ι2
⊢ (w' ∘ (⇑f : (a : ι2) → ι)) i = w i

Tactic:
simp_all only [comp_apply]

Premises used: Function.comp_apply
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
⊢ Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)

Tactic:
have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
hs' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)
rw : w i0 = w' ((f : (a : ι2) → ι) i0)
rw₁ rw₂ : w i0 = w i0
⊢ w i0 = 0

Tactic:
rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']

Premises used: Iff.mpr, Finset.mem_map', DFunLike.coe
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
intro intro₁ intro₂ intro₃ intro₄ intro₅ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
intro₆ intro₇ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
intro₈ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs),
    let w' : (i : ι) → k := fun (i : ι) ↦
      if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
      else 0;
    ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2), w i0 = 0
intro₉ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs),
    let fs' := map f fs;
    let w' : (i : ι) → k := fun (i : ι) ↦
      if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
      else 0;
    ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2) (hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0),
      w i0 = 0
intro₁₀ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs),
    let fs' := map f fs;
    let w' : (i : ι) → k := fun (i : ι) ↦
      if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
      else 0;
    ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2) (hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0)
      (hs' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)), w i0 = 0
⊢ AffineIndependent.{u_1, u_2, u_3, u_5} k (ι := ι2) (p ∘ (⇑f : (a : ι2) → ι))

Tactic:
classical
    intro fs w hw hs i0 hi0
    let fs' := fs.map f
    let w' i := if h : ∃ i2, f i2 = i then w h.choose else 0
    have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
    have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
    have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
    rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), 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
p : ι → P
ha : AffineIndependent k p
s : Set ι
⊢ AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (i : (↑s : Type u_4)) ↦ p (↑i : ι)

Tactic:
ha.comp_embedding (Embedding.subtype _)

Premises used: AffineIndependent.comp_embedding, Function.Embedding.subtype
-- 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
p : ι → P
ha : AffineIndependent k p
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
⊢ ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)

Tactic:
have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
-- 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
p : ι → P
ha : AffineIndependent k p
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)
fe : Embedding.{u_3 + 1, u_4 + 1} (↑(Set.range p) : Type u_3) ι := { toFun := f, inj' := ⋯ }
⊢ AffineIndependent k (ι := (↑(Set.range p) : Type u_3)) (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι))

Tactic:
ha.comp_embedding fe

Premises used: AffineIndependent.comp_embedding
-- 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
p : ι → P
ha : AffineIndependent k p
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)
fe : Embedding.{u_3 + 1, u_4 + 1} (↑(Set.range p) : Type u_3) ι := { toFun := f, inj' := ⋯ }
h :
  ∀ (x : (↑(Set.range p) : Type u_3)),
    Eq (α := (self : { x : P // x ∈ Set.range p }) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ Set.range p))
      (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι))
⊢ AffineIndependent k (P := P) fun (x : (↑(Set.range p) : Type u_3)) ↦ (↑x : P)

Tactic:
convert! ha.comp_embedding fe

Premises used: AffineIndependent.comp_embedding
-- 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
p : ι → P
ha : AffineIndependent k p
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)
fe : Embedding.{u_3 + 1, u_4 + 1} (↑(Set.range p) : Type u_3) ι := { toFun := f, inj' := ⋯ }
x : (↑(Set.range p) : Type u_3)
h : ∀ (x : { x : P // x ∈ Set.range p }), (↑x : P) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι)) x
⊢ Eq (α := (self : { x : P // x ∈ Set.range p }) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ Set.range p))
    (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι))

Tactic:
ext
-- 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
p : ι → P
ha : AffineIndependent k p
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)
fe : Embedding.{u_3 + 1, u_4 + 1} (↑(Set.range p) : Type u_3) ι := { toFun := f, inj' := ⋯ }
x : (↑(Set.range p) : Type u_3)
x_1 : { x : P // x ∈ Set.range p }
⊢ (↑x_1 : P) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι)) x_1

Tactic:
simp [fe, hf]
-- 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
ι' : Type u_5
e : ι ≃ ι'
p : ι' → P
⊢ AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι')) ↔ AffineIndependent k p

Tactic:
⟨?_, AffineIndependent.comp_embedding e.toEmbedding⟩

Premises used: AffineIndependent.comp_embedding, Equiv.toEmbedding, Iff.intro