mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e'_3
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ a = (fun i ↦ a + ↑i * δ') 0

Tactic:
;

Goal state after:
case e'_3
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ a = (fun i ↦ a + ↑i * δ') 0
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e'_4.e'_6
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ ↑i + 1 = ↑(i + 1)

Tactic:
;

Goal state after:
case e'_4.e'_6
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ ↑i + 1 = ↑(i + 1)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case inr.x
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ a + ↑i * δ' + 1 * δ' < a + ↑i * δ' + δ

Tactic:
;

Goal state after:
case inr.x
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ a + ↑i * δ' + 1 * δ' < a + ↑i * δ' + δ
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n : ℕ
hz : z = 1
⊢ 1 ≤ ‖z‖

Tactic:
;

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n : ℕ
hz : z = 1
⊢ 1 ≤ ‖z‖
Module: Mathlib.Analysis.Normed.Module.Extr

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
⊢ ‖f x + y‖ ≤ ‖f c + y‖

Tactic:
;

Goal state after:
α : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
⊢ ‖f x + y‖ ≤ ‖f c + y‖
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e'_4
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ b = a + (↑n + 1) * ((b - a) / (↑n + 1))

Tactic:
;

Goal state after:
case e'_4
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ b = a + (↑n + 1) * ((b - a) / (↑n + 1))
Module: Mathlib.Analysis.Normed.Module.Extr

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
⊢ ‖f x + y‖ ≤ ‖f c + y‖

Tactic:
hy.norm_add,

Goal state after:
α : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
⊢ ‖f x + y‖ ≤ ‖f c‖ + ‖y‖
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := ⋯
this✝¹ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this✝ :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1)).PairwiseDisjoint fun i ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ uIoc c (I i).1 ⊆ uIoc a b

Tactic:
;

Goal state after:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := ⋯
this✝¹ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this✝ :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1)).PairwiseDisjoint fun i ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ uIoc c (I i).1 ⊆ uIoc a b
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := ⋯
this✝¹ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this✝ :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1)).PairwiseDisjoint fun i ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ uIoc c (I i).2 ⊆ uIoc a b

Tactic:
;

Goal state after:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := ⋯
this✝¹ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this✝ :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1)).PairwiseDisjoint fun i ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ uIoc c (I i).2 ⊆ uIoc a b
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case h
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
a✝ : i ∈ range B₁
⊢ ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤ ‖l - s (i + 1)‖

Tactic:
;

Goal state after:
case h
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
a✝ : i ∈ range B₁
⊢ ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤ ‖l - s (i + 1)‖
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
a✝ : i ∈ range B₁
⊢ ‖z‖ ^ i ≤ 1

Tactic:
;

Goal state after:
case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
a✝ : i ∈ range B₁
⊢ ‖z‖ ^ i ≤ 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1))

Tactic:
;

Goal state after:
case succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1))
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ ≤ F + 1

Tactic:
;

Goal state after:
case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ ≤ F + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Tactic:
;

Goal state after:
θ : ℂ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π

Tactic:
;

Goal state after:
θ : ℂ
⊢ sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, ↑k * ↑π / 2 = θ

Tactic:
;

Goal state after:
θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, ↑k * ↑π / 2 = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
hθ : cos θ ≠ 0
⊢ (∃ k, θ = ↑k * ↑π) ∨ False ↔ ∃ k, ↑k * ↑π = θ

Tactic:
;

Goal state after:
θ : ℂ
hθ : cos θ ≠ 0
⊢ (∃ k, θ = ↑k * ↑π) ∨ False ↔ ∃ k, ↑k * ↑π = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁.mp
y : ℂ
k : ℤ
⊢ ∃ k_1, y = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + y)

Tactic:
;

Goal state after:
case h₁.mp
y : ℂ
k : ℤ
⊢ ∃ k_1, y = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h
y : ℂ
k : ℤ
⊢ y = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + y)

Tactic:
;

Goal state after:
case h
y : ℂ
k : ℤ
⊢ y = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁.mpr
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)

Tactic:
;

Goal state after:
case h₁.mpr
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h
x : ℂ
k : ℤ
⊢ x = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + x)

Tactic:
;

Goal state after:
case h
x : ℂ
k : ℤ
⊢ x = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + x)
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case inl
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
w : ℂ
hd : DiffContOnCl ℂ f (ball w (dist w w))
hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w
⊢ ‖f w‖ = ‖f w‖

pp: case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ ‖f w‖ = ‖f z‖

Tactic:
;

Goal state after:
case inl
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
w : ℂ
hd : DiffContOnCl ℂ f (ball w (dist w w))
hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w
⊢ ‖f w‖ = ‖f w‖

case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ ‖f w‖ = ‖f z‖
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case inl
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hw : dist z z ≤ r
⊢ (norm ∘ f) z = Function.const E ‖f z‖ z

pp: case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
;

Goal state after:
case inl
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hw : dist z z ≤ r
⊢ (norm ∘ f) z = Function.const E ‖f z‖ z

case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ ∀ (x : E), (norm ∘ f)⁻¹ x = (norm ∘ f⁻¹) x

Tactic:
;

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ ∀ (x : E), (norm ∘ f)⁻¹ x = (norm ∘ f⁻¹) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ z = ↑z.re + ↑z.im * I

Tactic:
;

Goal state after:
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ z = ↑z.re + ↑z.im * I
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ z = ↑z.re + ↑z.im * I

Tactic:
exact (re_add_im z).symm

Goal state after:
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

pp: case inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ frontier U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
;

Goal state after:
case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

case inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ frontier U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z