awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid

Tactic:
have h : s.points i = (-n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid := by
    rw [← neg_vsub_eq_vsub_rev, neg_smul_neg, ← point_vsub_centroid_eq_smul_vsub, vsub_vadd]
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
h : s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid
h₁ :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i})
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i}) (s.points i)

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
h : s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i})
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid)

Tactic:
smul_vsub_vadd_mem_affineSpan_pair _ _ _

Premises used: Set.Mem, smul_vsub_vadd_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
h : s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i})
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid)

Tactic:
exact smul_vsub_vadd_mem_affineSpan_pair _ _ _

Premises used: smul_vsub_vadd_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Finite ι
b : AffineBasis ι k P
⊢ FiniteDimensional k V

Tactic:
let ⟨i⟩ := b.nonempty
  (b.basisOf i).finiteDimensional_of_finite

Premises used: _private.0.AffineBasis.finiteDimensional.match_1, Module.Basis.finiteDimensional_of_finite, FiniteDimensional, AffineBasis.basisOf, AffineBasis.nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : FiniteDimensional k V
b : AffineBasis ι k P
⊢ Finite ι

Tactic:
finite_of_fin_dim_affineIndependent k b.ind

Premises used: AffineBasis.ind, finite_of_fin_dim_affineIndependent
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : FiniteDimensional k V
s : Set ι
b : AffineBasis.{u₁, u₂, u₃, u₄} (↑s : Type u₁) k P
⊢ s.Finite

Tactic:
finite_set_of_fin_dim_affineIndependent k b.ind

Premises used: AffineBasis.ind, finite_set_of_fin_dim_affineIndependent
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
b : AffineBasis ι k P
⊢ Fintype.card ι = Module.finrank k V + 1

Tactic:
have : FiniteDimensional k V := b.finiteDimensional
  b.ind.affineSpan_eq_top_iff_card_eq_finrank_add_one.mp b.tot

Premises used: AffineBasis.finiteDimensional, AffineBasis.tot, AffineBasis.ind, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one, Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
obtain :
  ∀ (s : Set P) (b : AffineBasis (↑s : Type u₄) k P)
    (hb : Eq (α := (a : (↑s : Type u₄)) → P) (⇑b : (a : (↑s : Type u₄)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))),
    Nonempty (AffineBasis ι k P)
⊢ Nonempty (AffineBasis ι k P)

Tactic:
obtain ⟨s, b, hb⟩ := AffineBasis.exists_affineBasis k V P

Premises used: AffineBasis.exists_affineBasis
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Set P
b : AffineBasis (↑s : Type u₄) k P
hb : Eq (α := (a : (↑s : Type u₄)) → P) (⇑b : (a : (↑s : Type u₄)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
⊢ s.Finite

Tactic:
b.finite_set

Premises used: AffineBasis.finite_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Set P
b : AffineBasis (↑s : Type u₄) k P
hb : Eq (α := (a : (↑s : Type u₄)) → P) (⇑b : (a : (↑s : Type u₄)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
lift :
  ∀ (s : Finset P) (b : AffineBasis (↑(↑s : Set P) : Type u₄) k P)
    (hb :
      Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
        (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))),
    Nonempty (AffineBasis ι k P)
⊢ Nonempty (AffineBasis ι k P)

Tactic:
lift s to Finset P using b.finite_set

Premises used: Finset, AffineBasis.finite_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑(↑s : Set P) : Type u₄) k P
hb :
  Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
    (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))
⊢ Nonempty (AffineBasis ι k P)

Tactic:
⟨b.reindex <| Fintype.equivOfCardEq ?_⟩

Premises used: AffineBasis.reindex, Nonempty.intro, Fintype.equivOfCardEq
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑(↑s : Set P) : Type u₄) k P
hb :
  Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
    (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))
refine : Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Fintype.card ι
⊢ Nonempty (AffineBasis ι k P)

Tactic:
refine ⟨b.reindex <| Fintype.equivOfCardEq ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑(↑s : Set P) : Type u₄) k P
hb :
  Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
    (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))
rw : Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Module.finrank k V + 1
rw₁ rw₂ : Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄)
⊢ Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Fintype.card ι

Tactic:
rw [h, ← b.card_eq_finrank_add_one]

Premises used: AffineBasis.card_eq_finrank_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Module.Finite R V
inst_5 : Module.Free R V
inst_6 : AffineSpace V P
inst_7 : AddCommGroup W
inst_8 : Module R W
inst_9 : Module S W
inst_10 : Module.Finite S W
inst_11 : SMulCommClass R S W
⊢ Module.Finite S (P →ᵃ[R] W)

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
  .equiv <| (AffineMap.toConstProdLinearMap S).symm ≪≫ₗ (AffineEquiv.vaddConst R p).congrLeftₗ S W

Premises used: LinearEquiv.symm, AffineMap.toConstProdLinearMap, AffineEquiv.vaddConst, inferInstance, AffineMap, AffineEquiv.congrLeftₗ, _private.0.AffineBasis.finiteDimensional.match_1, Module.Finite, Module.Finite.equiv, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Module.Finite R V
inst_5 : Module.Free R V
inst_6 : AffineSpace V P
inst_7 : AddCommGroup W
inst_8 : Module R W
inst_9 : Module S W
inst_10 : Module.Finite S W
inst_11 : SMulCommClass R S W
inst_12 : Module.Free S W
inst_13 : StrongRankCondition R
inst_14 : StrongRankCondition S
rw : Module.finrank S W + Module.finrank R V * Module.finrank S W = (Module.finrank R V + 1) * Module.finrank S W
⊢ Module.finrank S (W × (V →ₗ[R] W)) = (Module.finrank R V + 1) * Module.finrank S W

Tactic:
rw [Module.finrank_prod, Module.finrank_linearMap]

Premises used: Module.finrank_linearMap, Module.finrank_prod
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Module.Finite R V
inst_5 : Module.Free R V
inst_6 : AffineSpace V P
inst_7 : AddCommGroup W
inst_8 : Module R W
inst_9 : Module S W
inst_10 : Module.Finite S W
inst_11 : SMulCommClass R S W
inst_12 : Module.Free S W
inst_13 : StrongRankCondition R
inst_14 : StrongRankCondition S
⊢ Module.finrank S W + Module.finrank R V * Module.finrank S W = (Module.finrank R V + 1) * Module.finrank S W

Tactic:
ring
-- 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
⊢ AffineIndependent k p ↔
    ∀ (s : Finset ι) (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V) → ∀ i ∈ s, w i = 0

Tactic:
Iff.rfl

Premises used: AffineIndependent, Iff.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 : Subsingleton ι
p : ι → P
⊢ AffineIndependent k p

Tactic:
fun _ _ h _ i hi => Fintype.eq_of_subsingleton_of_sum_eq h i hi

Premises used: AffineIndependent, Fintype.eq_of_subsingleton_of_sum_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 : Fintype ι
p : ι → P
mp :
  AffineIndependent k p →
    ∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
mpr :
  (∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0) →
    AffineIndependent k p
⊢ AffineIndependent k p ↔
    ∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0

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 : Fintype ι
p : ι → P
⊢ AffineIndependent k p →
    ∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0

Tactic:
fun h w hw hs i => h Finset.univ w hw hs i (Finset.mem_univ _)

Premises used: Finset.mem_univ, Finset.univ
-- 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 : Fintype ι
p : ι → P
⊢ AffineIndependent k p →
    ∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0

Tactic:
exact fun h w hw hs i => h Finset.univ w hw hs i (Finset.mem_univ _)
-- 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 : Fintype ι
p : ι → P
h :
  ∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
hi : i ∈ s
mpr :
  ∀ (hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V))
    (i : ι) (hi : i ∈ s), w i = 0
⊢ w i = 0

Tactic:
rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs

Premises used: Finset.weightedVSub_indicator_subset, Finset.subset_univ
-- 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 : Fintype ι
p : ι → P
h :
  ∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V)
i : ι
hi : i ∈ s
mpr :
  ∀ (hw : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V))
    (i : ι) (hi : i ∈ s), w i = 0
⊢ w i = 0

Tactic:
rw [← Finset.sum_indicator_subset _ (Finset.subset_univ s)] at hw

Premises used: Finset.sum_indicator_subset, Finset.subset_univ
-- 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 : Fintype ι
p : ι → P
h :
  ∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 0
hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V)
i : ι
hi : i ∈ s
⊢ (↑s : Set ι).indicator w i = 0

Tactic:
replace h := h ((↑s : Set ι).indicator w) hw hs 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
inst_4 : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 0
hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V)
i : ι
hi : i ∈ s
h : (↑s : Set ι).indicator w i = 0
⊢ w i = 0

Tactic:
simpa [hi] using h
-- 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
v : V
⊢ AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p

Tactic:
simp +contextual [AffineIndependent, weightedVSub_vadd]

Premises used: AffineIndependent, Finset.weightedVSub_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
G : Type u_5
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
p : ι → V
a : G
⊢ AffineIndependent k (a • p) ↔ AffineIndependent k p

Tactic:
simp +contextual [AffineIndependent,
    ← smul_comm (α := V) a, ← smul_sum, smul_eq_zero_iff_eq]

Premises used: smul_eq_zero_iff_eq, AffineIndependent, Finset.smul_sum, SMulCommClass.smul_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
p : ι → P
i1 : ι
mp :
  AffineIndependent k p →
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
mpr :
  (LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1) →
    AffineIndependent k p
⊢ AffineIndependent k p ↔
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1

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
p : ι → P
i1 : ι
h : AffineIndependent k p
mp :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1

Tactic:
rw [linearIndependent_iff']

Premises used: linearIndependent_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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0
i : { x : ι // x ≠ i1 }
hi : i ∈ s
⊢ let f : ι → k := fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx);
  f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)

Tactic:
set f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩ with hfdef

Premises used: dite, Subtype.mk, Eq, Finset.sum, Neg.neg
-- 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
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0
i : { x : ι // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
⊢ ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)

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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0
i : { x : ι // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
⊢ ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)

Tactic:
have hfg : ∀ x : { x // x ≠ i1 }, g x = f x := by 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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0
i : { x : ι // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
mp : f (↑i : ι) = 0
⊢ g i = 0

Tactic:
rw [hfg]
-- 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
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0
i : { x : ι // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
rw : f i1 + ∑ x ∈ s, g x = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ ι ∈ s2, f ι) 0

Tactic:
rw [Finset.sum_insert
            (Finset.notMem_map_subtype_of_not_property s (Classical.not_not.2 rfl)),
          Finset.sum_subtype_map_embedding fun x _ => (hfg x).symm]

Premises used: Iff.mpr, Classical.not_not, Finset.sum_subtype_map_embedding, Finset.sum_insert, Eq.symm, rfl, Finset.notMem_map_subtype_of_not_property
-- 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
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0
i : { x : ι // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
rw :
  HAdd.hAdd (α := k)
      ((fun (x : ι) ↦ (if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx) : k)) i1)
      (∑ x ∈ s, g x) =
    0
⊢ f i1 + ∑ x ∈ s, g x = 0

Tactic:
rw [hfdef]