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

Goal state before:
pp: case inr
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
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
]

Goal state after:
case inr
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
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
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
  apply Set.Subset.antisymm
  · intro p hp
    obtain hp' := Set.mem_of_mem_of_subset hp s.closedInterior_subset_affineSpan
    obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp'
    rw [Set.mem_union, or_iff_not_imp_left]
    intro h
    rw [affineCombination_mem_closedInterior_iff hw1] at hp
    simp_rw [affineCombination_mem_interior_iff hw1, Set.mem_Ioo] at h
    push +distrib Not at h
    obtain ⟨j, hj⟩ : ∃ j : Fin (n + 1), w j = 0 := by
      obtain ⟨i, hi | hi⟩ := h
      · exact ⟨i, le_antisymm hi (hp i).1⟩
      · have hi1 : w i = 1 := le_antisymm (hp i).2 hi
        rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1
        exact ⟨i + 1, hw1 _ (by simp)⟩
    refine Set.mem_iUnion.mpr ⟨j, ?_⟩
    rw [faceOpposite, affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1]
    exact ⟨fun k _ ↦ hp k, by simpa using hj⟩
  · refine Set.union_subset s.interior_subset_closedInterior (Set.iUnion_subset fun i ↦ ?_)
    exact s.closedInterior_faceOpposite_subset_closedInterior i

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
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
⊢ ∑ i ∈ Finite.toFinset hfin_w, w i.down • z i.down ∈ 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
ι : 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
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
⊢ ∑ i ∈ Finite.toFinset hfin_w, w i.down • z i.down ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
]

Goal state after:
case inr
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) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
Module: Mathlib.Topology.NhdsKer

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

Tactic:
]

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
⊢ ⋂₀ {t | IsOpen[inst✝] t ∧ s ⊆ t} ⊆ t

Tactic:
]

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen[inst✝] t
⊢ ⋂₀ {t | IsOpen[inst✝] t ∧ s ⊆ t} ⊆ t
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_1
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
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
h₁ : ∑ i ∈ Finite.toFinset hfin_w, w i.down = 1
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
⊢ ∑ i ∈ Finite.toFinset hfin_w, w i.down = 1

Tactic:
]

Goal state after:
case refine_1
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
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
h₁ : ∑ i ∈ Finite.toFinset hfin_w, w i.down = 1
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
⊢ ∑ i ∈ Finite.toFinset hfin_w, w i.down = 1
Module: Mathlib.Topology.NhdsKer

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

Tactic:
]

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

Goal state before:
pp: case refine_2
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
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
i : PLift ι
hi : i ∈ support (w ∘ PLift.down)
⊢ w i.down ≠ 0

Tactic:
]

Goal state after:
case refine_2
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
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
i : PLift ι
hi : i ∈ support (w ∘ PLift.down)
⊢ w i.down ≠ 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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 : AffineIndependent k fun p ↦ ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
]

Goal state after:
case inr
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 : AffineIndependent k fun p ↦ ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
Module: Mathlib.Topology.NhdsKer

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

Tactic:
]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst✝¹] (⋂₀ {t | IsOpen[inst✝¹] t ∧ s ⊆ t})

Tactic:
]

Goal state after:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst✝¹] (⋂₀ {t | IsOpen[inst✝¹] t ∧ s ⊆ t})
Module: Mathlib.Topology.AlexandrovDiscrete

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

Tactic:
]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ y ∈ s

Tactic:
]

Goal state after:
case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ y ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val

Tactic:
]

Goal state after:
case inr
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : ∃ i ∈ S, (nhdsKer {a} ∩ i).Nonempty
⊢ a ∈ ⋃₀ S

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : ∃ i ∈ S, (nhdsKer {a} ∩ i).Nonempty
⊢ a ∈ ⋃₀ S
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
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : 1 < t
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ ⇑(AffineMap.lineMap x y) '' openSegment 𝕜 0 t

Tactic:
]

Goal state after:
𝕜 : 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
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : 1 < t
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ ⇑(AffineMap.lineMap x y) '' openSegment 𝕜 0 t
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[inst✝¹] (⋂ t ∈ S, f ⁻¹' t)

Tactic:
]

Goal state after:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst✝¹] s
⊢ IsOpen[inst✝¹] (⋂ t ∈ S, f ⁻¹' t)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr.refine_1
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ b ⊆ ⇑(Equiv.vaddConst p).symm '' s

Tactic:
]

Goal state after:
case inr.refine_1
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ b ⊆ ⇑(Equiv.vaddConst p).symm '' s
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 (⇑(∑ x, (LinearMap.proj x).smulRight ↑x) '' stdSimplex 𝕜 ↑s)

Tactic:
]

Goal state after:
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 (⇑(∑ x, (LinearMap.proj x).smulRight ↑x) '' stdSimplex 𝕜 ↑s)
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ (lineMap x y) t⁻¹ ∈ (fun x_1 ↦ (lineMap x y) x_1⁻¹) '' Ioi 1

Tactic:
]

Goal state after:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ (lineMap x y) t⁻¹ ∈ (fun x_1 ↦ (lineMap x y) x_1⁻¹) '' Ioi 1
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr.refine_2
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b) = affineSpan k s

Tactic:
]

Goal state after:
case inr.refine_2
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b) = affineSpan k s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocallyPathConnectedSpace X
hF : IsOpen[inst✝¹] F
x : X
⊢ ∀ x_1 ∈ pathComponentIn F x, pathComponentIn F x ∈ 𝓝 x_1

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocallyPathConnectedSpace X
hF : IsOpen[inst✝¹] F
x : X
⊢ ∀ x_1 ∈ pathComponentIn F x, pathComponentIn F x ∈ 𝓝 x_1
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ IsOpen[inst✝¹] (pathComponentIn univ x)

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ IsOpen[inst✝¹] (pathComponentIn univ x)
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
⊢ connectedComponent y = connectedComponent x ↔ y ∈ connectedComponent x

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
⊢ connectedComponent y = connectedComponent x ↔ y ∈ connectedComponent x
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : x ≠ y → (interior s).Nonempty
⊢ (interior s).Nonempty

Tactic:
]

Goal state after:
case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : x ≠ y → (interior s).Nonempty
⊢ (interior s).Nonempty
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mpr.inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 {x}
hx : x ∈ ∅
⊢ {x}.Nontrivial

Tactic:
]

Goal state after:
case mpr.inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 {x}
hx : x ∈ ∅
⊢ {x}.Nontrivial
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyPathConnectedSpace X
e : Y → X
he : IsOpenEmbedding e
this : ∀ (y : Y), (𝓝 y).HasBasis (fun s ↦ s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) fun x ↦ e ⁻¹' x
x : Y
s : Set X
x✝ : s ∈ 𝓝 (e x) ∧ IsPathConnected s ∧ s ⊆ range e
left✝ : s ∈ 𝓝 (e x)
hs : IsPathConnected s
hse : s ⊆ range e
⊢ IsPathConnected s

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyPathConnectedSpace X
e : Y → X
he : IsOpenEmbedding e
this : ∀ (y : Y), (𝓝 y).HasBasis (fun s ↦ s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) fun x ↦ e ⁻¹' x
x : Y
s : Set X
x✝ : s ∈ 𝓝 (e x) ∧ IsPathConnected s ∧ s ⊆ range e
left✝ : s ∈ 𝓝 (e x)
hs : IsPathConnected s
hse : s ⊆ range e
⊢ IsPathConnected s
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr.refine_2.hd
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ insert ((Equiv.vaddConst p).symm p) (⇑(Equiv.vaddConst p).symm ∘ ⇑(Equiv.vaddConst p) '' b) = insert 0 b

Tactic:
]

Goal state after:
case inr.refine_2.hd
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ insert ((Equiv.vaddConst p).symm p) (⇑(Equiv.vaddConst p).symm ∘ ⇑(Equiv.vaddConst p) '' b) = insert 0 b
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
U_op : IsOpen[inst✝¹] U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑U

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
U_op : IsOpen[inst✝¹] U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑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
s : Set E
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : ∑ i ∈ t, w i < 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass (-w) z ∈ (convexHull R) s

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
s : Set E
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : ∑ i ∈ t, w i < 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass (-w) z ∈ (convexHull R) s