mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
e p q e' p' q' : ℕ
hp : n e ≤ p
hq : n e ≤ q
hp' : n e' ≤ p'
hq' : n e' ≤ q'
he' : e ≤ e'
r : ℕ := max (n e) (n e')
I : (1 / 2) ^ e' ≤ (1 / 2) ^ e
J1 : ‖L e p q - L e p r‖ ≤ 4 * ‖c‖ * (1 / 2) ^ e
J2 : ‖L e p r - L e' p' r‖ ≤ 4 * ‖c‖ * (1 / 2) ^ e
J3 : ‖L e' p' r - L e' p' q'‖ ≤ 4 * ‖c‖ * (1 / 2) ^ e
⊢ 4 * ‖c‖ * (1 / 2) ^ e + 4 * ‖c‖ * (1 / 2) ^ e + 4 * ‖c‖ * (1 / 2) ^ e = 12 * ‖c‖ * (1 / 2) ^ e

Tactic:
by ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))

pp: x : ℝ
h : |x| < 1
⊢ Summable fun n ↦ x ^ (n + 1) / (↑n + 1)

Tactic:
]

Goal state after:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))

x : ℝ
h : |x| < 1
⊢ Summable fun n ↦ x ^ (n + 1) / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
⊢ Tendsto (fun e ↦ ‖∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)

Tactic:
]

Goal state after:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e ↦ ‖∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ x + r • y ∈ s

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ x + r • y ∈ s
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ |x| ^ (i + 1) / (↑i + 1) = |x| ^ (i + 1) / (↑i + 1)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
⊢ ↑c * (μ F + ε / ↑c) ≤ ↑c * (μ F + ε / ↑c)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Tactic:
]

Goal state after:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (L0 n) (L0 N) < ε

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (L0 n) (L0 N) < ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))

pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ x ∉ Set.range fun x ↦ 2 * x, term x = 0

Tactic:
]

Goal state after:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))

x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ x ∉ Set.range fun x ↦ 2 * x, term x = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
⊢ ↑c * μ F + ε = ↑c * μ F + ε

pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
⊢ ↑c ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
⊢ ↑c ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ term m = 0

Tactic:
]

Goal state after:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ term m = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∫⁻ (a : α), ↑(f₁ a) + ↑(f₂ a) ∂μ ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∫⁻ (a : α), ↑(f₁ a) + ↑(f₂ a) ∂μ ≠ ∞
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : r * c ≤ ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩

Tactic:
]

Goal state after:
case refine_2.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : r * c ≤ ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1

pp: a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1

pp: a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)

Tactic:
]

Goal state after:
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1

a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1

a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))

pp: case hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0

pp: case hy
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0

Tactic:
]

Goal state after:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))

case hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0

case hy
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2.inr.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + 0 • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x ∈ s
⊢ 0 ≤ ↑f ⟨x, hx⟩

Tactic:
]

Goal state after:
case refine_2.inr.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
hy' : 0 • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + 0 • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x ∈ s
⊢ 0 ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / (12 * ‖c‖)
e' : ℕ
he' : e' ≥ e
⊢ ‖L0 e - L0 e'‖ < ε

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / (12 * ‖c‖)
e' : ℕ
he' : e' ≥ e
⊢ ‖L0 e - L0 e'‖ < ε
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ x + r • y ∈ s

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ x + r • y ∈ s
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
⊢ gauge s (-x) = gauge s (-x)

Tactic:
]

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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
ha : 0 ≤ 0
hx : x ∈ 0 • s
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case add
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (a : α), ↑(f₁ a) ∂μ + ∫⁻ (a : α), ↑(f₂ a) ∂μ ≤ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ + ε

Tactic:
]

Goal state after:
case add
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (a : α), ↑(f₁ a) ∂μ + ∫⁻ (a : α), ↑(f₂ a) ∂μ ≤ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ + ε
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2.inr.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : r * c ≤ ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩

Tactic:
]

Goal state after:
case refine_2.inr.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : r * c ≤ ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
⊢ r⁻¹ • x ∈ s

Tactic:
]

Goal state after:
case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
⊢ r⁻¹ • x ∈ s
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
hp : n e ≤ p
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ‖L e (n e) p - L0 b‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
hp : n e ≤ p
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ‖L e (n e) p - L0 b‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : x ∈ δ • s
this : r⁻¹ • x ∈ s
⊢ r⁻¹ • x ∈ s

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : x ∈ δ • s
this : r⁻¹ • x ∈ s
⊢ r⁻¹ • x ∈ s