mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ LinearIndependent k fun i ↦ ![p₁, p₂] ↑i -ᵥ ![p₁, p₂] 0

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ LinearIndependent k fun i ↦ ![p₁, p₂] ↑i -ᵥ ![p₁, p₂] 0
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
⊢ (∀ (x : X) (u : Set X), IsOpen[inst✝] u → IsOpen[inst✝] (pathComponentIn u x)) ↔
    ∀ (x : X) (u : Set X), IsOpen[inst✝] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace X
⊢ (∀ (x : X) (u : Set X), IsOpen[inst✝] u → IsOpen[inst✝] (pathComponentIn u x)) ↔
    ∀ (x : X) (u : Set X), IsOpen[inst✝] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ ∑ i ∈ t, w i • (p i -ᵥ 0) = ∑ i ∈ t, w i • p i

Tactic:
]

Goal state after:
R : Type u_1
E : Type u_3
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ ∑ i ∈ t, w i • (p i -ᵥ 0) = ∑ i ∈ t, w i • p i
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a ⊔ 𝓝[>] a

Tactic:
]

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a ⊔ 𝓝[>] a
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ s.centerMass w v ∈ (convexHull R) (Set.range v)

Tactic:
]

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ s.centerMass w v ∈ (convexHull R) (Set.range v)
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous[inst✝¹, x✝] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst✝¹] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
hx' : x ∈ f ⁻¹' u
⊢ f '' pathComponentIn (f ⁻¹' u) x ⊆ pathComponentIn u (f x)

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous[inst✝¹, x✝] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst✝¹] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
hx' : x ∈ f ⁻¹' u
⊢ f '' pathComponentIn (f ⁻¹' u) x ⊆ pathComponentIn u (f x)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ ![p₁, p₂] ↑i₁ -ᵥ ![p₁, p₂] 0 ≠ 0

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ ![p₁, p₂] ↑i₁ -ᵥ ![p₁, p₂] 0 ≠ 0
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a

Tactic:
]

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
⊢ ∀ (x : X ⊕ Y) (u : Set (X ⊕ Y)), IsOpen[instTopologicalSpaceSum] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
⊢ ∀ (x : X ⊕ Y) (u : Set (X ⊕ Y)), IsOpen[instTopologicalSpaceSum] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
hs : s.Nonempty
⊢ s.centerMass (centroidWeights R s) id ∈ (convexHull R) ↑s

Tactic:
]

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
hs : s.Nonempty
⊢ s.centerMass (centroidWeights R s) id ∈ (convexHull R) ↑s
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case hw₀
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
hs : s.Nonempty
⊢ ∀ i ∈ s, 0 ≤ centroidWeights R s i

Tactic:
simp only [inv_nonneg, imp_true_iff, Nat.cast_nonneg, Finset.centroidWeights_apply]

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
x : X ⊕ Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
hxu : x ∈ u
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSum] t ∧ x ∈ t

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
x : X ⊕ Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
hxu : x ∈ u
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSum] t ∧ x ∈ t
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : s ∩ Iio a = ∅
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[>] a

Tactic:
]

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : s ∩ Iio a = ∅
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[>] a
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in ⊥, s \ {a} ∈ 𝓝 x

Tactic:
]

Goal state after:
case inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in ⊥, s \ {a} ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
⊢ ∀ (x : (i : ι) × X i) (u : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x

Tactic:
]

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
⊢ ∀ (x : (i : ι) × X i) (u : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t

Tactic:
]

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case inr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
⊢ (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
⊢ (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ x ∈ s with x ≠ i, wm x + ∑ x ∈ s with ¬x ≠ i, wm x = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x ↦ wm ↑x
⊢ ∑ x ∈ s with x ≠ i, wm x = 1

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ x ∈ s with x ≠ i, wm x + ∑ x ∈ s with ¬x ≠ i, wm x = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x ↦ wm ↑x
⊢ ∑ x ∈ s with x ≠ i, wm x = 1
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst✝¹⁴ : Field 𝕜
inst✝¹³ : LinearOrder 𝕜
inst✝¹² : IsStrictOrderedRing 𝕜
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : OrderClosedTopology 𝕜
inst✝⁹ : CompactIccSpace 𝕜
inst✝⁸ : ContinuousAdd 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : ContinuousSMul 𝕜 V
inst✝² : AffineSpace V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsCompact ((convexHull 𝕜) (range (s.map ↑(AffineEquiv.vaddConst 𝕜 (s.points 0)).symm ⋯).points))

Tactic:
]

Goal state after:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst✝¹⁴ : Field 𝕜
inst✝¹³ : LinearOrder 𝕜
inst✝¹² : IsStrictOrderedRing 𝕜
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : OrderClosedTopology 𝕜
inst✝⁹ : CompactIccSpace 𝕜
inst✝⁸ : ContinuousAdd 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : ContinuousSMul 𝕜 V
inst✝² : AffineSpace V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsCompact ((convexHull 𝕜) (range (s.map ↑(AffineEquiv.vaddConst 𝕜 (s.points 0)).symm ⋯).points))
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ i ∈ s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x ↦ wm ↑x
hw' : ∑ x ∈ s', w' x = 1
⊢ ((affineCombination k (Finset.subtype (fun x ↦ x ≠ i) s) fun i_1 ↦ p ↑i_1) fun i_1 ↦ wm ↑i_1) ∈
    affineSpan k (Set.range (p ∘ Subtype.val))

Tactic:
]

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ i ∈ s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x ↦ wm ↑x
hw' : ∑ x ∈ s', w' x = 1
⊢ ((affineCombination k (Finset.subtype (fun x ↦ x ≠ i) s) fun i_1 ↦ p ↑i_1) fun i_1 ↦ wm ↑i_1) ∈
    affineSpan k (Set.range (p ∘ Subtype.val))
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
hU : ∃ «I», «I».Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ «I».pi t ⊆ U
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ U

Tactic:
]

Goal state after:
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
hU : ∃ «I», «I».Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ «I».pi t ⊆ U
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ U
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ (s ∪ s').sum W = 1

Tactic:
rw [sum_add_distrib, ← sum_subset subset_union_left,
        ← sum_subset subset_union_right, sum_ite_of_true,
        sum_ite_of_true, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
        mul_one]

Goal state after:
case h
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ ∀ x ∈ s', x ∈ s'

case h
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ ∀ x ∈ s, x ∈ s

R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) = 0

R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
⊢ ∀ i ∈ s, w i = 0

Tactic:
]

Goal state after:
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
⊢ ∀ i ∈ s, w i = 0
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
⊢ IsPathConnected (univ.pi (K.piecewise (fun i ↦ pathComponentIn (t i) (x i)) fun x ↦ univ))

Tactic:
]

Goal state after:
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
⊢ IsPathConnected (univ.pi (K.piecewise (fun i ↦ pathComponentIn (t i) (x i)) fun x ↦ univ))
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case pos
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∈ K
⊢ IsPathConnected (pathComponentIn (t i) (x i))

Tactic:
]

Goal state after:
case pos
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∈ K
⊢ IsPathConnected (pathComponentIn (t i) (x i))
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
⊢ 0 = 0

pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
⊢ ∀ x ∈ s, w x ≠ 0 → x ≠ i

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
⊢ ∀ x ∈ s, w x ≠ 0 → x ≠ i