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

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ AbsolutelyContinuousOnInterval (f • g) a b

Tactic:
unfold AbsolutelyContinuousOnInterval at hf hg

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ AbsolutelyContinuousOnInterval (f • g) a b
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y

Tactic:
convert (hf.mono_of_mem_nhdsWithin hs).hasDerivWithinAt

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ iteratedDerivWithin (k + 2) f s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
⊢ ↑K * (ε / (↑K + 1)) < (↑K + 1) * (ε / (↑K + 1))

Tactic:
by gcongr; linarith

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
⊢ ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C

Tactic:
rintro y ⟨hay, hyx⟩

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case a
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)
δ' : ℝ := ⋯
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) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))) ∈ disjWithin a b

Tactic:
constructor

Goal state after:
case a.left
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)
δ' : ℝ := ⋯
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) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ ∀ i ∈ Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1,
    ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ∈ uIcc a b ∧ ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2 ∈ uIcc a b

case a.right
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)
δ' : ℝ := ⋯
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) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ (↑(Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1)).PairwiseDisjoint fun i ↦
    uIoc ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : M ≤ 1
⊢ stolzSet M = ∅

Tactic:
by
  ext z
  rw [stolzSet, Set.mem_ofPred, Set.mem_empty_iff_false, iff_false, not_and, not_lt, ← sub_pos]
  intro zn
  calc
    _ ≤ 1 * (1 - ‖z‖) := by gcongr
    _ = ‖(1 : ℂ)‖ - ‖z‖ := by rw [one_mul, norm_one]
    _ ≤ _ := norm_sub_norm_le _ _

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk✝ : k ≤ n
hk : k < n
⊢ ↑k.succ ≤ ↑n

Tactic:
by norm_cast

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

Goal state before:
pp: case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : z ∈ {z | 1 - ε < z.re}
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M

Tactic:
rw [Set.mem_ofPred_eq, sub_lt_comm, ← one_re, ← sub_re] at hzl

Goal state after:
case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x + y‖ ≤ 2 - δ'

Tactic:
calc
    ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ := by
      have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
      rw [norm_sub_rev, norm_sub_rev y', this]
      exact norm_add₃_le
    _ ≤ 2 - δ + δ' + δ' := by
      gcongr
      exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]
    _ ≤ 2 - δ' := by
      suffices δ' ≤ δ / 3 by linarith
      exact min_le_of_right_le <| min_le_right _ _

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
f : α → β
inst✝ : DecidablePred fun x ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
⊢ ((∏ x ∈ s with f x ≤ 0, -1) * ∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x

Tactic:
Finset.prod_const_one,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
f : α → β
inst✝ : DecidablePred fun x ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
⊢ (∏ x ∈ s with f x ≤ 0, -1) * 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

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

Tactic:
constructor

Goal state after:
case mp
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) → ∃ k, θ = ↑k * ↑π

case mpr
θ : ℂ
⊢ (∃ k, θ = ↑k * ↑π) → ∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) ↔ ∃ k, y = ↑k * ↑π * 2 + x

Tactic:
constructor

Goal state after:
case h₁.mp
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) → ∃ k, y = ↑k * ↑π * 2 + x

case h₁.mpr
x y : ℂ
⊢ (∃ k, y = ↑k * ↑π * 2 + x) → ∃ k, x = ↑k * ↑π * 2 + y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ ((∃ n, ↑n * (2 * π) = x) ∨ ∃ k, π + ↑k * (2 * π) = x) ↔ ∃ k, ↑k * π = x

Tactic:
constructor

Goal state after:
case mp
x : ℝ
⊢ ((∃ n, ↑n * (2 * π) = x) ∨ ∃ k, π + ↑k * (2 * π) = x) → ∃ k, ↑k * π = x

case mpr
x : ℝ
⊢ (∃ k, ↑k * π = x) → (∃ n, ↑n * (2 * π) = x) ∨ ∃ k, π + ↑k * (2 * π) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ ((∃ k, π / 2 + ↑k * (2 * π) = x) ∨ ∃ k, -(π / 2) + ↑k * (2 * π) = x) ↔ ∃ k, π / 2 + ↑k * π = x

Tactic:
constructor

Goal state after:
case mp
x : ℝ
⊢ ((∃ k, π / 2 + ↑k * (2 * π) = x) ∨ ∃ k, -(π / 2) + ↑k * (2 * π) = x) → ∃ k, π / 2 + ↑k * π = x

case mpr
x : ℝ
⊢ (∃ k, π / 2 + ↑k * π = x) → (∃ k, π / 2 + ↑k * (2 * π) = x) ∨ ∃ k, -(π / 2) + ↑k * (2 * π) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)

Tactic:
constructor

Goal state after:
case left
⊢ -(π / 2) < π / 4

case right
⊢ π / 4 < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x < -1
⊢ arctan x + arctan x = arctan (2 * x / (1 - x ^ 2)) - π

Tactic:
arctan_add_eq_sub_pi (by nlinarith) (by linarith)

Goal state after:
x : ℝ
h : x < -1
⊢ arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - x ^ 2)) - π
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x y : ℝ
⊢ |(cexp (↑(x - y) * I)).arg| = |toIocMod Real.two_pi_pos (-π) (x - y)|

Tactic:
arg_exp_mul_I

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))

Tactic:
real_inner_comm,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪y, x⟫ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 ↔ ⟪x, y⟫ = 0

Tactic:
constructor

Goal state after:
case mp
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 → ⟪x, y⟫ = 0

case mpr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ = 0 → ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ π / 2 ∈ Icc 0 π

Tactic:
constructor

Goal state after:
case left
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ 0 ≤ π / 2

case right
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ π / 2 ≤ π
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
⊢ {x | x ≠ 0} = (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x✝ : 𝕜
⊢ x✝ ∈ {x | x ≠ 0} ↔ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ = {0}ᶜ

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x✝ : 𝕜
⊢ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ ↔ x✝ ∈ {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_2.convert_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ = fun x ↦ x = 0 → False

Tactic:
ext

Goal state after:
case refine_2.convert_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x✝ : 𝕜
⊢ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ ↔ x✝ ∈ fun x ↦ x = 0 → False
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
⊢ (fun g ↦ g ≠ 0) = fun x ↦ x ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := ⋯
x✝ : 𝕜
⊢ x✝ ≠ 0 ↔ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
⊢ (zpowGroupHom (-↑n)).ker = (powMonoidHom n).ker

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ x✝ ∈ (zpowGroupHom (-↑n)).ker ↔ x✝ ∈ (powMonoidHom n).ker
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ x✝ ^ (-↑n) = (⇑(Homeomorph.inv 𝕜ˣ) ∘ fun x ↦ x ^ n) x✝

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ ↑(x✝ ^ (-↑n)) = ↑((⇑(Homeomorph.inv 𝕜ˣ) ∘ fun x ↦ x ^ n) x✝)
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ star (star z) = z

Tactic:
ext

Goal state after:
z : 𝔻
⊢ ↑(star (star z)) = ↑z
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝕔𝔻
⊢ star (star z) = z

Tactic:
ext

Goal state after:
z : 𝕔𝔻
⊢ ↑(star (star z)) = ↑z
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
⊢ f =ᶠ[𝓝[≠] x] 0

Tactic:
rw [← hf.frequently_zero_iff_eventuallyEq_zero]
  apply ((accPt_iff_frequently_nhdsNE.1 h₂x).and_eventually <| eventually_mem_set.2
    (mem_codiscreteWithin_iff_forall_mem_nhdsNE.1 h x h₁x)).mono
  simp +contextual

Goal state after:
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g} ∧ U ⊆ {x | f =ᶠ[𝓝[≠] x] g}

Tactic:
constructor

Goal state after:
case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g}

case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ U ⊆ {x | f =ᶠ[𝓝[≠] x] g}
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g}

Tactic:
apply isOpen_setOfPred_eventually_nhdsWithin

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ (divisor f₁ U) z = (divisor f₂ U) z

Tactic:
rw [divisor_apply hf₁ hz, divisor_apply hf₂ hz]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ (meromorphicOrderAt f₁ z).untop₀ = (meromorphicOrderAt f₂ z).untop₀
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : ¬MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U

Tactic:
· ext x
    by_cases hx : x ∈ U
    · simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin h₁ h₂]
      congr 1
      apply meromorphicOrderAt_congr
      simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
        disjoint_principal_right] at h₁
      have : U ∈ 𝓝[≠] x := by
        apply mem_nhdsWithin.mpr
        use U, h₂, hx, Set.inter_subset_left
      filter_upwards [this, h₁ x hx] with a h₁a h₂a
      simp only [Set.mem_compl_iff, Set.mem_sdiff, Set.mem_ofPred_eq, not_and] at h₂a
      tauto
    · simp [hx]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : ¬MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ MeromorphicNFAt f x → AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0 → MeromorphicNFAt f x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ 0 ≤ meromorphicOrderAt f x ↔ AnalyticAt 𝕜 f x

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ 0 ≤ meromorphicOrderAt f x → AnalyticAt 𝕜 f x

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ AnalyticAt 𝕜 f x → 0 ≤ meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ meromorphicOrderAt f x = 0 ↔ f x ≠ 0

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ meromorphicOrderAt f x = 0 → f x ≠ 0

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ f x ≠ 0 → meromorphicOrderAt f x = 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
⊢ f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
⊢ f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g