mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s - t)

Tactic:
rw [sub_eq_add_neg]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s + -t)
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)

pp: case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hvx : v ≠ x
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)

Tactic:
· refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_
    rw [Convex.combo_self hab, singleton_add]
    exact
      (isOpenMap_add_left _).image_interior_subset _
        (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hvx : v ≠ x
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
f g : Seminorm 𝕜 E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨_⟩⟩
    rcases g with ⟨⟨_⟩⟩
    congr

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

Goal state before:
pp: case refine_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥

Tactic:
rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' ∅)
⊢ (⨆ p, ⇑↑p) (x + y) ≤ (⨆ p, ⇑↑p) x + (⨆ p, ⇑↑p) y

Tactic:
simp [Real.iSup_of_isEmpty]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₂ ∥ s₁

Tactic:
rcases h with ⟨v, rfl⟩

Goal state after:
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
s₁ : AffineSubspace k P
v : V
⊢ map (↑(constVAdd k P v)) s₁ ∥ s₁
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ s₁ ∥ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁)

Tactic:
refine ⟨v₂₃ + v₁₂, ?_⟩

Goal state after:
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
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁) = map (↑(constVAdd k P (v₂₃ + v₁₂))) s₁
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₁.direction = s₂.direction

Tactic:
rcases h with ⟨v, rfl⟩

Goal state after:
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
s₁ : AffineSubspace k P
v : V
⊢ s₁.direction = (map (↑(constVAdd k P v)) s₁).direction
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_nonempty k h

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

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₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
h₁₂₄₅ : ∃ z, z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
h₂₃₅₆ : line[k, p₅, p₆].direction ≤ line[k, p₂, p₃].direction
h₃₁₆₄ : line[k, p₆, p₄].direction ≤ line[k, p₃, p₁].direction
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
direction_affineSpan_pair_le_iff_exists_smul

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₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
h₁₂₄₅ : ∃ z, z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
h₂₃₅₆ : ∃ z, z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
h₃₁₆₄ : ∃ z, z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ {y | ↑(s.sup fun i ↦ NNReal.mk ((p i) (y - x)) ⋯) ≤ ↑r} = {x_1 | ∀ i ∈ s, (p i) (x_1 - x) ≤ ↑r}

Tactic:
NNReal.coe_le_coe,

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ {y | (s.sup fun i ↦ NNReal.mk ((p i) (y - x)) ⋯) ≤ r} = {x_1 | ∀ i ∈ s, (p i) (x_1 - x) ≤ ↑r}
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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
⊢ ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = 0

Tactic:
← hs

Goal state after:
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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
⊢ ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)

Tactic:
refine subset_antisymm smul_closedBall_subset ?_
  intro x
  rw [Set.mem_smul_set, Seminorm.mem_closedBall_zero]
  refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
  · rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, inv_mul_le_iff₀ hk]
  rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓝 0 ≤ 𝓝 0

Tactic:
· rw [(@NormedAddGroup.nhds_zero_basis_norm_lt E
      p.toAddGroupSeminorm.toSeminormedAddGroup).le_basis_iff hb]
    simpa only [subset_def, mem_ball_zero] using! h₂

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Metric.closedBall 0 r)

Tactic:
← closedBall_normSeminorm 𝕜

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).closedBall 0 r)
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a b : E
⊢ range ⇑(Path.segment a b) = [a -[ℝ] b]

Tactic:
rw [segment_eq_image_lineMap, image_eq_range]
  simp only [← segment_apply]

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✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
hn : ¬Injective fun s ↦ affineSpan k (p '' s)
⊢ False

Tactic:
not_injective_iff

Goal state after:
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
hn : ∃ a b, affineSpan k (p '' a) = affineSpan k (p '' b) ∧ a ≠ b
⊢ False
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
hx : x ∈ stdSimplex ℝ ι
y : ι → ℝ
hy : y ∈ stdSimplex ℝ ι
i : ι
⊢ dist (x i) (y i) ≤ 1

Tactic:
have hx := mem_Icc_of_mem_stdSimplex hx i

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
hx✝ : x ∈ stdSimplex ℝ ι
y : ι → ℝ
hy : y ∈ stdSimplex ℝ ι
i : ι
hx : x i ∈ Icc 0 1
⊢ dist (x i) (y i) ≤ 1
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
⊢ False

Tactic:
let fs' : Finset ι := insert i (insert j (fs.map (Embedding.subtype _)))

Goal state after:
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_1
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✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hw' : ∀ (i : Fin (m + 1)), w i ∈ Set.Icc 0 1
hs : (affineCombination k univ (s.face h).points) w = s.points j
⊢ s.points j ∈ affineSpan k (s.points '' ↑fs)

Tactic:
← hs

Goal state after:
case refine_1
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✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hw' : ∀ (i : Fin (m + 1)), w i ∈ Set.Icc 0 1
hs : (affineCombination k univ (s.face h).points) w = s.points j
⊢ (affineCombination k univ (s.face h).points) w ∈ affineSpan k (s.points '' ↑fs)
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:
congr! with ⟨x, y⟩ _; rw [nhdsKer_pair]

Goal state after:
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₃ : LinearIndependent k Subtype.val
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val

Tactic:
linearIndependent_set_iff_affineIndependent_vadd_union_singleton k hb₀ p

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.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
⊢ {p} ∪ ⇑(Equiv.vaddConst p) '' b ⊆ s

Tactic:
apply Set.union_subset (Set.singleton_subset_iff.mpr hp)

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
⊢ ⇑(Equiv.vaddConst p) '' b ⊆ s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
z : X
⊢ z ∈ V → z ∈ (pathComponent x)ᶜ

Tactic:
hz

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
z : X
hz : z ∈ V
⊢ z ∈ (pathComponent x)ᶜ
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : Field 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : ZeroLEOneClass 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst✝³] t
⊢ ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
by
  let : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
  have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1
  rw [← uniformity_eq_comap_nhds_zero] at this
  rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩
  refine ⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex,
    subset_add_left _ hV0, subset_add_left _ hV0, ?_⟩
  simp_rw [← iUnion_add_left_image, image_add_left]
  simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV
  exact hV

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
s : Finset E
x : E
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ↔
    ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x

Tactic:
refine exists_congr fun w ↦ and_congr_right' <| and_congr_right fun hw ↦ ?_

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
x : E
w : E → R
hw : ∑ y ∈ s, w y = 1
⊢ s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}

Tactic:
simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected {y | ∃ r, 0 < r ∧ r • x = y}
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
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∃ i, ∃ (_ : ↑i ⊆ s), t.centerMass w z ∈ (convexHull R) ↑i

Tactic:
refine ⟨t.image z, ?_, ?_⟩

Goal state after:
case refine_1.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
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ↑(Finset.image z t) ⊆ s

case refine_1.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
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass w z ∈ (convexHull R) ↑(Finset.image z t)
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y z : E
hy : y ∈ segment ℝ x z
⊢ ‖y - x‖ ≤ ‖z - x‖

Tactic:
by
  rw [segment_eq_image'] at hy
  simp only [mem_image, mem_Icc] at hy
  obtain ⟨u, ⟨hu_nonneg, hu_le_one⟩, rfl⟩ := hy
  simp only [add_sub_cancel_left, norm_smul, Real.norm_eq_abs]
  rw [abs_of_nonneg hu_nonneg]
  conv_rhs => rw [← one_mul (‖z - x‖)]
  gcongr

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy✝ : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp✝ : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
χ : α
hp : p χ
hy : dist (y χ) x < δ
⊢ dist (z χ) x < δ → ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
hz

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy✝ : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz✝ : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp✝ : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
χ : α
hp : p χ
hy : dist (y χ) x < δ
hz : dist (z χ) x < δ
⊢ ∀ v ∈ [y χ -[ℝ] z χ], r χ v
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case fst
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ (∑ i, (fun p ↦ w p.1 * v p.2) i • (fun p ↦ (f p.1, g p.2)) i).1 = (x, y).1

Tactic:
simp_rw [Prod.fst_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_comm (w _), mul_smul,
      sum_comm (γ := ι), ← Fintype.sum_smul_sum, hv₁, one_smul, hf]

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
⊢ ∑ j, ∑ g, (∏ k, w k (↑g k)) • f i (↑g i) = ∑ x, ∑ i_1, (∏ k, w k (↑i_1 k)) • f i x

Tactic:
congr! with j _ g _

Goal state after:
case a.a
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
j : κ i
a✝¹ : j ∈ Finset.univ
g : { g // g i = j }
a✝ : g ∈ Finset.univ
⊢ ↑g i = j