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✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
c : k
⊢ (affineCombination k s p) w = (AffineMap.lineMap ((affineCombination k s p) w₁) ((affineCombination k s p) w₂)) c ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i)) c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝¹³ : Ring 𝕜
inst✝¹² : LinearOrder 𝕜
inst✝¹¹ : IsStrictOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ ↦ (1 - θ) • x + θ • y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝¹³ : Ring 𝕜
inst✝¹² : LinearOrder 𝕜
inst✝¹¹ : IsStrictOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure (openSegment 𝕜 x y) = [x -[𝕜] y]

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ interior (a • s) + closure (b • s) = interior (a • s) + b • s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
i : Fin (n + 1)
hw1 : ∀ i_1 ∈ univ.erase i, w i_1 = 0
hi : 1 ≤ w i
hi1 : w i = 1
⊢ i + 1 ∈ univ.erase i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • closure s + b • interior s ⊆ interior s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ∃ i, w i ≤ 0 ∨ 1 ≤ w i
⊢ ∃ j, w j = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • s ⊆ interior s

Tactic:
exact hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab)

Goal state after:
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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∀ v ∈ Basis.ofVectorSpaceIndex k V, v ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • s + b • interior s ⊆ interior s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
by

Goal state after:
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
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
⊢ (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s

Tactic:
by

Goal state after:
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
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∑ i ∈ t, w i • z i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ∃ i, w i ≤ 0 ∨ 1 ≤ w i
j : Fin (n + 1)
hj : w j = 0
⊢ ∀ i ∉ {j}ᶜ, w i = 0

Tactic:
by

Goal state after:
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
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ HasFiniteSupport (w ∘ PLift.down)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : AddRightMono 𝕜
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • (y - x) ∈ interior s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : AddRightMono 𝕜
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : x + y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • y ∈ interior s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
⊢ s.closedInterior = s.interior ∪ ⋃ i, (s.faceOpposite i).closedInterior

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
⊢ s.closedInterior \ s.interior = ⋃ i, (s.faceOpposite i).closedInterior

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ZeroLEOneClass 𝕜
s : Set E
hs : IsOpen s
⊢ IsOpen ((convexHull 𝕜) s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
⊢ nhdsKer {x} = (𝓝 x).ker

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x y : X
⊢ x ∈ nhdsKer {y} ↔ x ⤳ y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ nhdsKer s ↔ ∀ (U : Set X), IsOpen[inst✝] U → s ⊆ U → x ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ⊆ nhdsKer t ↔ ∀ (U : Set X), IsOpen[inst✝] U → t ⊆ U → s ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen[inst✝] t
⊢ nhdsKer s ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Sort u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
⊢ nhdsKer (⋃ i, s i) = ⋃ i, nhdsKer (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_3
s : Set ι
t : ι → Set X
⊢ nhdsKer (⋃ i ∈ s, t i) = ⋃ i ∈ s, nhdsKer (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
S : Set (Set X)
⊢ nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ nhdsKer s ↔ x ∈ nhdsKer (⋃ y ∈ s, {y})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ nhdsKer (⋃ y ∈ s, {y}) ↔ ∃ y ∈ s, x ⤳ y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ nhdsKer s ⊆ nhdsKer t ↔ 𝓝ˢ s ≤ 𝓝ˢ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ nhdsKer s = nhdsKer t ↔ 𝓝ˢ s = 𝓝ˢ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ nhdsKer {x} ⊆ nhdsKer {y}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ s = ∅ → nhdsKer s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (nhdsKer s) = 𝓝ˢ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ nhdsKer (nhdsKer s) = nhdsKer s

Tactic:
by

Goal state after:
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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
⊢ ∀ v ∈ h.extend ⋯, v ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ nhdsKer {(x, y)} = nhdsKer {x} ×ˢ nhdsKer {y}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ ⋃ p ∈ s ×ˢ t, nhdsKer {p} = ⋃ p ∈ s ×ˢ t, nhdsKer {p.1} ×ˢ nhdsKer {p.2}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ (⋃ x ∈ s, nhdsKer {x}) ×ˢ ⋃ y ∈ t, nhdsKer {y} = nhdsKer s ×ˢ nhdsKer t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
p : (i : ι) → X i
⊢ nhdsKer {p} = univ.pi fun i ↦ nhdsKer {p i}

Tactic:
by

Goal state after:
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
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ nhdsKer (univ.pi s) = ⋃ p ∈ univ.pi s, nhdsKer {p}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ ⋃ p ∈ univ.pi s, nhdsKer {p} = ⋃ p ∈ univ.pi s, univ.pi fun i ↦ nhdsKer {p i}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (univ.pi fun i ↦ ⋃ x ∈ s i, nhdsKer {x}) = univ.pi fun i ↦ nhdsKer (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
⊢ StrictConvex 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.NhdsKer

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen (U i)
⊢ (nhdsKer s ⊆ ⋃ i, U i → ∃ t, nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔ s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
simp only [(isOpen_iUnion hUo).nhdsKer_subset,
    (isOpen_iUnion fun i ↦ isOpen_iUnion fun _ ↦ hUo i).nhdsKer_subset]

Goal state after:
Module: Mathlib.Topology.Compactness.NhdsKer

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact (nhdsKer s) ↔ IsCompact s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst✝] s) → IsClosed[inst✝] (⋃₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : IndiscreteTopology α
⊢ ∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen[inst✝²] s) → IsOpen[inst✝²] (⋂₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
f : ι → Set α
⊢ (closure[inst✝¹] (⋃ i, f i))ᶜ = (⋃ i, closure[inst✝¹] (f i))ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ closure[inst✝¹] (⋃₀ S) = ⋃ s ∈ S, closure[inst✝¹] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[inst✝¹] s
⊢ IsOpen[inst✝¹] (⋂₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst✝¹] (nhdsKer s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ nhdsKer s ⊆ s ↔ IsOpen[inst✝¹] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ nhdsKer s ⊆ s ↔ IsOpen[inst✝¹] s

Tactic:
by
  simp only [nhdsKer_eq_iff_isOpen.symm, Subset.antisymm_iff, subset_nhdsKer, and_true]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
t : Set α
a : α
⊢ nhdsKer {a} ⊆ t ↔ t ∈ 𝓝 a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s t : Set α
⊢ nhdsKer s ⊆ t ↔ s ⊆ interior t

Tactic:
by

Goal state after:
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
s : Set P
h : AffineIndependent k fun p ↦ ↑p
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ 𝓟 (nhdsKer s) = 𝓝ˢ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ([x -[𝕜] y] \ frontier s).Nonempty
⊢ StrictConvex 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
a : α
⊢ 𝓟 (nhdsKer {a}) = 𝓝 a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
⊢ AlexandrovDiscrete α

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) = interior s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst✝¹] s
⊢ IsOpen[coinduced f inst✝¹] (⋂₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
s : Set E
⊢ (closedConvexHull 𝕜) (closure s) ⊆ (closedConvexHull 𝕜) s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a✝ a : α
⊢ 𝓝 a = generate {nhdsKer {a}}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: E : Type u_3
𝕜 : Type u_4
inst✝¹¹ : Field 𝕜
inst✝¹⁰ : LinearOrder 𝕜
inst✝⁹ : IsStrictOrderedRing 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : OrderClosedTopology 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Finite
⊢ IsCompact ((convexHull 𝕜) s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ AlexandrovDiscrete (α × β)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι✝ : Sort u_1
κ : ι✝ → Sort u_2
α : Type u_3
β : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AlexandrovDiscrete α
inst✝³ : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst✝² : Finite ι
X : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), AlexandrovDiscrete (X i)
⊢ AlexandrovDiscrete ((i : ι) → X i)

Tactic:
by

Goal state after: