mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.StdSimplex

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

Tactic:
grind [Real.dist_eq]

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

Goal state before:
pp: case refine_2
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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
x✝ : p ∈ Simplex.setInterior I s
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h : (affineCombination k univ s.points) w = p
⊢ p ∈ Simplex.setInterior I (s.reindex e)

Tactic:
subst h
    rw [← Function.comp_id w, ← Function.comp_id s.points, ← e.symm_comp_self,
      ← Function.comp_assoc, ← Function.comp_assoc, ← e.coe_toEmbedding,
      ← Finset.univ.affineCombination_map e.toEmbedding, map_univ_equiv]
    change Finset.univ.affineCombination k (s.reindex e).points _ ∈ _
    have hw' : ∑ i, (w ∘ e.symm) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
    rw [affineCombination_mem_setInterior_iff hw']
    exact fun i ↦ hwI (e.symm i)

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

Goal state before:
pp: case e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ ∑ i ∈ t with w i ≠ 0, w i • z i = ∑ i ∈ t' with w' i ≠ 0, w' i • z' i

Tactic:
· exact sum_congr (by grind) (by grind)

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✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
⊢ w i ∈ Set.Icc 0 1

Tactic:
by_cases hi : i ∈ fs

Goal state after:
case pos
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✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i ∈ Set.Icc 0 1

case neg
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✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∉ fs
⊢ w i ∈ Set.Icc 0 1
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:
rintro _ ⟨a, b, ha, hb, hab, rfl⟩
  exact hs.combo_closure_interior_mem_interior hx hy ha.le hb hab

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, ∃ t, IsOpen[inst✝²] t ∧ f ⁻¹' t = s
⊢ ∃ t, IsOpen[inst✝²] t ∧ f ⁻¹' t = ⋂₀ S

Tactic:
choose U hU htU using hS

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst✝²] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ ∃ t, IsOpen[inst✝²] t ∧ f ⁻¹' t = ⋂₀ S
Module: Mathlib.Topology.Connected.LocallyPathConnected

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

Tactic:
by
  rw [← pathComponentIn_univ]
  exact isOpen_univ.pathComponentIn _

Goal state after:
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
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ Ioo b a ⊆ s

Tactic:
exact hs.Ioo_subset_of_mem_closure (subset_closure hbs) has

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

Tactic:
rcases eq_empty_or_nonempty (s ∩ Iio a) with hs' | ⟨b, hbs, hba⟩

Goal state after:
case inl
𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
hs' : s ∩ Iio a = ∅
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

case inr
𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
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 (s.map ↑(AffineEquiv.vaddConst 𝕜 (s.points 0)).symm ⋯).closedInterior

Tactic:
← convexHull_eq_closedInterior

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.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_2
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
hW₁ : (s ∪ s').sum W = 1
⊢ ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) • v x = 0

Tactic:
intro i _ hi'

Goal state after:
case refine_2.refine_2
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
hW₁ : (s ∪ s').sum W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : i ∉ s'
⊢ (if i ∈ s' then b * w' i else 0) • v i = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_2
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
hW₁ : (s ∪ s').sum W = 1
⊢ ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) • v x = 0

Tactic:
intro i _ hi'

Goal state after:
case refine_2.refine_2
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
hW₁ : (s ∪ s').sum W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : i ∉ s
⊢ (if i ∈ s then a * w i else 0) • v i = 0
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
inst✝ : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
h₁ : (fun x ↦ p ↑x) = fun x ↦ f ↑x
h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i}
⊢ AffineIndependent k f

Tactic:
replace ha : AffineIndependent k fun x : {x | x ≠ i} ↦ f x := h₁ ▸ AffineIndependent.subtype ha _

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
inst✝ : DecidableEq ι
p : ι → P
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
h₁ : (fun x ↦ p ↑x) = fun x ↦ f ↑x
h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i}
ha : AffineIndependent k fun x ↦ f ↑x
⊢ AffineIndependent k f
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: case inr.inl.refine_1
R : Type u_1
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
x : R
hl : ∃ b, b < x
hu : IsTop x
inst✝ : OrderTop R
i✝ : R
a✝ : i✝ < ⊤
⊢ ∃ i', (i' ∈ 𝓝 ⊤ ∧ Convex R i') ∧ id i' ⊆ Ioi i✝

Tactic:
refine ⟨Set.Ioi _, ?_, subset_rfl⟩

Goal state after:
case inr.inl.refine_1
R : Type u_1
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
x : R
hl : ∃ b, b < x
hu : IsTop x
inst✝ : OrderTop R
i✝ : R
a✝ : i✝ < ⊤
⊢ Ioi i✝ ∈ 𝓝 ⊤ ∧ Convex R (Ioi i✝)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_3
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
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ i ∈ sx.disjSum sy, Sum.elim zx zy i ∈ s

Tactic:
· intro i hi
      rw [Finset.mem_disjSum] at hi
      rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩) <;> apply_rules [hzx, hzy]

Goal state after:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ ∃ f, mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)

Tactic:
by
  rcases (mkCLM K E).toLinearMap.exists_rightInverse_of_surjective
    (LinearMap.range_eq_top.mpr surjective_mk) with ⟨f, hf⟩
  replace hf : mk ∘ f = id := congr_arg DFunLike.coe hf
  exact ⟨⟨f, isInducing_mk.continuous_iff.2 (by continuity)⟩, DFunLike.ext' hf⟩

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

Goal state before:
pp: case hb
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := ⋯
hc : w j / c + w k / c = 1
⊢ f ((w j / c) • p j + (w k / c) • p k) < (w j / c) • f (p j) + (w k / c) • f (p k)

Tactic:
refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc

Goal state after:
case hb.refine_1
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ 0 < w j / c

case hb.refine_2
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ 0 < w k / c
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mpr
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h : p ∈ s.closedInterior
⊢ ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p

Tactic:
· obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
      Set.mem_of_mem_of_subset h s.closedInterior_subset_affineSpan
    rw [affineCombination_mem_closedInterior_iff hw1] at h
    exact ⟨Finset.univ, w, fun i _ ↦ (h i).1, hw1, rfl⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ WithSeminorms fun p ↦ ↑p

Tactic:
have hp' (i : ι) : Continuous (p i) := hp.continuous_seminorm i

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
⊢ WithSeminorms fun p ↦ ↑p
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (𝓝 ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0)) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Tactic:
UniformOnFun.nhds_eq_of_basis _ _ h.uniformity_of_nhds_zero

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)
      (⨅ s ∈ 𝔖,
        ⨅ i,
          ⨅ (_ : p i),
            𝓟
              {g |
                ∀ x ∈ s,
                  ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0) x, (UniformOnFun.toFun 𝔖) g x) ∈
                    {x | x.2 - x.1 ∈ b i}}) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_3.refine_2.inl
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
r : ℝ
r_pos : 0 < r
hw : t = (∅.sup fun x ↦ p).ball 0 r
⊢ t ∈ 𝓝 0

Tactic:
simp only [ball, Finset.sup_empty, sub_zero, coe_bot, Pi.zero_apply, r_pos, ofPred_true] at hw

Goal state after:
case refine_3.refine_2.inl
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
r : ℝ
r_pos : 0 < r
hw : t = univ
⊢ t ∈ 𝓝 0
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
⊢ instUniformSpace σ F 𝔖₁ ≤ instUniformSpace σ F 𝔖₂

Tactic:
simp_rw [uniformSpace_eq]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
⊢ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖₁) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖₁) ≤
    UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖₂) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖₂)
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c⁻¹‖⁻¹ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Tactic:
inv_lt_one₀ (norm_pos_iff.2 <| inv_ne_zero h0)

Goal state after:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : ¬r < 0
⊢ ∃ x, ‖x‖ < 1 ∧ r < ‖f x‖

Tactic:
lift r to ℝ≥0 using not_lt.1 hr₀
    exact f.exists_lt_apply_of_lt_opNNNorm hr

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ WithSeminorms (q.comp f)

Tactic:
by
  rw [hf.eq_induced]
  exact f.withSeminorms_induced hq

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂✝ : Type u_2
inst✝³⁶ : NormedField 𝕜₁
inst✝³⁵ : NormedField 𝕜₂✝
σ : 𝕜₁ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
G✝ : Type u_5
inst✝³⁴ : AddCommGroup E✝
inst✝³³ : Module 𝕜₁ E✝
inst✝³² : TopologicalSpace E✝
inst✝³¹ : AddCommGroup F✝
inst✝³⁰ : Module 𝕜₂✝ F✝
𝕜 : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
𝕜₄ : Type u_9
E : Type u_10
F : Type u_11
G : Type u_12
H : Type u_13
inst✝²⁹ : AddCommGroup E
inst✝²⁸ : AddCommGroup F
inst✝²⁷ : AddCommGroup G
inst✝²⁶ : AddCommGroup H
inst✝²⁵ : NormedField 𝕜
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
inst✝²² : NormedField 𝕜₄
inst✝²¹ : Module 𝕜 E
inst✝²⁰ : Module 𝕜₂ F
inst✝¹⁹ : Module 𝕜₃ G
inst✝¹⁸ : Module 𝕜₄ H
inst✝¹⁷ : TopologicalSpace E
inst✝¹⁶ : TopologicalSpace F
inst✝¹⁵ : TopologicalSpace G
inst✝¹⁴ : TopologicalSpace H
inst✝¹³ : IsTopologicalAddGroup G
inst✝¹² : IsTopologicalAddGroup H
inst✝¹¹ : ContinuousConstSMul 𝕜₃ G
inst✝¹⁰ : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁷ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁶ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁵ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁴ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁₂ ⁻¹' t ∈ 𝔖
s : Set E
⊢ s ∈ 𝔖 → (fun x ↦ ⇑e₁₂ '' x) s ∈ 𝔗

Tactic:
simp [h, preimage_image_eq _ e₁₂.injective]

Goal state after: