mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Measurable f
⊢ Measurable fun p ↦ log ‖f (circleMap 0 R p.2) - circleMap 0 1 p.1‖

Tactic:
;

Goal state after:
f : ℂ → ℂ
R : ℝ
hf : Measurable f
⊢ Measurable fun p ↦ log ‖f (circleMap 0 R p.2) - circleMap 0 1 p.1‖
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
⊢ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
;

Goal state after:
case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
⊢ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal (↑l * (x - y))).toReal = ↑l * (x - y)
⊢ -(↑l * (x - y)) = ↑l * (y - x)

Tactic:
;

Goal state after:
case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal (↑l * (x - y))).toReal = ↑l * (x - y)
⊢ -(↑l * (x - y)) = ↑l * (y - x)
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ (convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ

Tactic:
rcases hx with (h | h)

Goal state after:
case inl
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
⊢ (convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ

case inr
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
⊢ (convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z y

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z y
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y

pp: case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y

Tactic:
· exact ⟨ws, zw, wy⟩

Goal state after:
case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
;

Goal state after:
case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
⊢ Function.Even (logCounting f e)

Tactic:
intro r

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
r : ℝ
⊢ logCounting f e (-r) = logCounting f e r
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ t ∩ Icc z y

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ t ∩ Icc z y
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
r : ℝ
hr : R₀ ≤ r
z : E
hz : z ∈ t
⊢ logCounting (single z 1) r = log r - log ‖z‖

Tactic:
;

Goal state after:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
r : ℝ
hr : R₀ ≤ r
z : E
hz : z ∈ t
⊢ logCounting (single z 1) r = log r - log ‖z‖
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
;

Goal state after:
case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ 0 ≤ 0 ∧ 0 ≤ s

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ 0 ≤ 0 ∧ 0 ≤ s
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
z : ↑s
v : 𝕜
⊢ L (v • (0, 1)) = L (0, v)

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
z : ↑s
v : 𝕜
⊢ L (v • (0, 1)) = L (0, v)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ affineSegment R x y ⊆ ↑line[R, x, y]

Tactic:
rw [affineSegment, Set.subset_def]
  rintro p ⟨r, -, rfl⟩
  exact lineMap_mem_affineSpan_pair _ _ _

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∈ s
hz : z ∈ s
ε : R
⊢ (lineMap x z) ε ∈ s

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∈ s
hz : z ∈ s
ε : R
⊢ (lineMap x z) ε ∈ s
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht : t ∈ Set.Icc 0 1
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ho : t ∈ Set.Ioo 0 1
⊢ (lineMap x z) t ∈ ⇑(lineMap x z) '' Set.Ioo 0 1

Tactic:
· exact ⟨t, ho, rfl⟩

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s = ∅
⊢ ∅.Countable ∧
    sSup ∅ = s.domRestrict φ ∧ ∀ f ∈ ∅, f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c

Tactic:
;

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s = ∅
⊢ ∅.Countable ∧
    sSup ∅ = s.domRestrict φ ∧ ∀ f ∈ ∅, f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s = ∅
⊢ sSup ∅ = fun x ↦ φ ↑x

Tactic:
;

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s = ∅
⊢ sSup ∅ = fun x ↦ φ ↑x
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
f : ℕ → ↑s → ℝ
hf : 𝓕' = range f
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hlc : ∀ (i : ℕ), f i = s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)
i : ℕ
x : ↑s
⊢ (s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)) x = f i x

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
f : ℕ → ↑s → ℝ
hf : 𝓕' = range f
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hlc : ∀ (i : ℕ), f i = s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)
i : ℕ
x : ↑s
⊢ (s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)) x = f i x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx - tx * ty + ty = 0 ∨ z -ᵥ x = 0
⊢ x = (lineMap x z) ty

Tactic:
rcases hx with (h | h)

Goal state after:
case mp.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : tx - tx * ty + ty = 0
⊢ x = (lineMap x z) ty

case mp.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z -ᵥ x = 0
⊢ x = (lineMap x z) ty
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case pos.refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ = 0
this : ∀ (a : ↑s), s.domRestrict φ a = 0 a
x✝ : ↑s
⊢ (⨆ i, s.domRestrict (⇑re ∘ ⇑((fun x ↦ 0) i)) + const (↑s) ((fun x ↦ 0) i)) x✝ = s.domRestrict φ x✝

Tactic:
;

Goal state after:
case pos.refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ = 0
this : ∀ (a : ↑s), s.domRestrict φ a = 0 a
x✝ : ↑s
⊢ (⨆ i, s.domRestrict (⇑re ∘ ⇑((fun x ↦ 0) i)) + const (↑s) ((fun x ↦ 0) i)) x✝ = s.domRestrict φ x✝
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ ≠ 0
x : ↑s
hx : s.domRestrict φ x ≠ 0 x
this : sSup 𝓕' x = s.domRestrict φ x
⊢ s = ∅

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ ≠ 0
x : ↑s
hx : s.domRestrict φ x ≠ 0 x
this : sSup 𝓕' x = s.domRestrict φ x
⊢ s = ∅
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
⊢ F.eventualRange i ⊆ ⇑(ConcreteCategory.hom (F.map f)) '' range ⇑(ConcreteCategory.hom (F.map g))

Tactic:
;

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
⊢ F.eventualRange i ⊆ ⇑(ConcreteCategory.hom (F.map f)) '' range ⇑(ConcreteCategory.hom (F.map g))
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s ↔
    x ∈ ⇑(ConcreteCategory.hom (F.map (g ≫ f))) ⁻¹' s

Tactic:
;

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s ↔
    x ∈ ⇑(ConcreteCategory.hom (F.map (g ≫ f))) ⁻¹' s