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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
t_meas : MeasurableSet t
⊢ μ t < ∞ → ∀ᵐ (x : α) ∂μ.restrict t, 0 x ≤ f x

Tactic:
t_lt_top

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
t_meas : MeasurableSet t
t_lt_top : μ t < ∞
⊢ ∀ᵐ (x : α) ∂μ.restrict t, 0 x ≤ f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
hy : y ∈ Iio x
⊢ slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc y x) y

Tactic:
replace hy : y ≤ x := hy.le

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
hy : y ≤ x
⊢ slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc y x) y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
hy : y ≤ x
this : -((y - x)⁻¹ • ∫ (t : ℝ) in Icc y x, f t) = (x - y)⁻¹ • ∫ (t : ℝ) in Icc y x, f t
⊢ slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc y x) y

Tactic:
by
      simpa [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_ge, hy, h]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case inr
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)
⊢ BoundedVariationOn f (Icc a b)

Tactic:
set δ' := (b - a) / (n + 1)

Goal state after:
case inr
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)
⊢ BoundedVariationOn f (Icc a b)
Module: Mathlib.Analysis.Complex.AbelLimit

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

Tactic:
by
  let s := fun n ↦ ∑ i ∈ range n, f i
  have k := h.sub (summable_powerSeries_of_norm_lt_one h.cauchySeq hz).hasSum.tendsto_sum_nat
  simp_rw [← sum_sub_distrib, ← mul_one_sub, ← geom_sum_mul_neg, ← mul_assoc, ← sum_mul,
    mul_comm, mul_sum _ _ (f _), range_eq_Ico, ← sum_Ico_Ico_comm', ← range_eq_Ico,
    ← sum_mul] at k
  conv at k =>
    enter [1, n]
    rw [sum_congr (g := fun j ↦ (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
      rfl (fun j hj ↦ by congr 1; exact sum_Ico_eq_sub _ (mem_range.mp hj))]
  suffices Tendsto (fun n ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0) by
    simp_rw [mul_sum] at this
    replace this := (this.const_mul (1 - z)).add k
    conv at this =>
      enter [1, n]
      rw [← mul_add, ← sum_add_distrib]
      enter [2, 2, i]
      rw [← add_mul, sub_add_sub_cancel]
    rwa [mul_zero, zero_add] at this
  rw [← zero_mul (-1 / (z - 1))]
  apply Tendsto.mul
  · simpa only [neg_zero, neg_sub] using (tendsto_sub_nhds_zero_iff.mpr h).neg
  · conv =>
      enter [1, n]
      rw [geom_sum_eq (by contrapose! hz; simp [hz]), sub_div, sub_eq_add_neg, ← neg_div]
    rw [← zero_add (-1 / (z - 1)), ← zero_div (z - 1)]
    apply Tendsto.add (Tendsto.div_const (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hz) (z - 1))
    simp only [zero_div, zero_add, tendsto_const_nhds_iff]

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

Goal state before:
pp: 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
⊢ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ ≤ ‖1 - z‖ * (F + 1)

Tactic:
gcongr; linarith only

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x y : ℂ
⊢ sin x = sin y ↔ ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x

Tactic:
by
  simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]
  refine exists_congr fun k => or_congr ?_ ?_ <;> refine Eq.congr rfl ?_ <;> simp [field] <;> ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x < 0
⊢ x < sin x

Tactic:
simpa using sin_lt <| neg_pos.2 hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ tan (arctan x) ^ 2 / (1 + tan (arctan x) ^ 2) = x ^ 2 / (1 + x ^ 2)

Tactic:
tan_arctan

Goal state after:
x : ℝ
⊢ x ^ 2 / (1 + x ^ 2) = x ^ 2 / (1 + x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ (1 + tan (arctan x) ^ 2)⁻¹ = (1 + x ^ 2)⁻¹

Tactic:
tan_arctan

Goal state after:
x : ℝ
⊢ (1 + x ^ 2)⁻¹ = (1 + x ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ tan (arctan x) / √(1 + tan (arctan x) ^ 2) = x / √(1 + x ^ 2)

Tactic:
tan_arctan

Goal state after:
x : ℝ
⊢ x / √(1 + x ^ 2) = x / √(1 + x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ cos (arctan x) = (√(1 + x ^ 2))⁻¹

Tactic:
← inv_sqrt_one_add_tan_sq (cos_arctan_pos x),

Goal state after:
x : ℝ
⊢ (√(1 + tan (arctan x) ^ 2))⁻¹ = (√(1 + x ^ 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ (√(1 + tan (arctan x) ^ 2))⁻¹ = (√(1 + x ^ 2))⁻¹

Tactic:
tan_arctan

Goal state after:
x : ℝ
⊢ (√(1 + x ^ 2))⁻¹ = (√(1 + x ^ 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = arctan (tan (arctan x))⁻¹

pp: case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

pp: case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2

Tactic:
tan_arctan

Goal state after:
x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = arctan x⁻¹

case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inr
x y : ℝ
hy : 0 < y
h : arctan x < arctan y⁻¹
⊢ arctan x + arctan y < π / 2

Tactic:
arctan_inv_of_pos hy,

Goal state after:
case inr
x y : ℝ
hy : 0 < y
h : arctan x < π / 2 - arctan y
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : π / 2 - arctan x + arctan y⁻¹ = arctan ((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π

Tactic:
arctan_inv_of_pos hy,

Goal state after:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : π / 2 - arctan x + (π / 2 - arctan y) = arctan ((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ IsMinOn f S x

Tactic:
refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx ?_ hf_rd.symm.le
  exact (hf.leftDeriv_le_rightDeriv_of_mem_interior hx).trans_eq hf_rd

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ f' < slope f x y

Tactic:
obtain ⟨u, hxu, huy⟩ := exists_between hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
⊢ f' < slope f x y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y < f'

Tactic:
obtain ⟨u, hxu, huy⟩ := exists_between hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
⊢ slope f x y < f'
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_1
⊢ IsQuotientMap fun z ↦ ⟨cexp z, ⋯⟩

Tactic:
refine IsOpenMap.isQuotientMap ?_ (by fun_prop) fun z ↦ ⟨_, Subtype.ext (exp_log z.2)⟩
    exact (IsOpen.isOpenEmbedding_subtypeVal isClosed_singleton.1).isOpenMap_iff.mpr isOpenMap_exp

Goal state after:
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
x✝ : 𝕜
⊢ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ ↔ x✝ ∈ fun x ↦ x = 0 → False

Tactic:
simpa using! (this _).not

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

Goal state before:
pp: case H
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
⊢ DifferentiableAt ℂ f c

Tactic:
exact hd.differentiableAt <| ball_mem_nhds _ h_R₁

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = ↑n
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
left

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = ↑n
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 f x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = ↑n
hn : n < 0
⊢ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
use hf

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = ↑n
hn : n < 0
⊢ meromorphicOrderAt f x < 0 ∧ f x = 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₁f : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt (g • f) x

Tactic:
left

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₁f : f =ᶠ[𝓝 x] 0
⊢ g • f =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
left

Goal state after:
case neg.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
⊢ f ^ n =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt f⁻¹ x

Tactic:
left

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x] 0
⊢ f⁻¹ =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : y ∈ {x}ᶜ
⊢ y - x ≠ 0 ∨
    -(meromorphicOrderAt f x).untop₀ + (meromorphicOrderAt f x).untop₀ ≠ 0 ∨
      -(meromorphicOrderAt f x).untop₀ = 0 ∧ (meromorphicOrderAt f x).untop₀ = 0

Tactic:
left

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : y ∈ {x}ᶜ
⊢ y - 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 : 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f x = 0 ↔ toMeromorphicNFAt f x x ≠ 0

Tactic:
simp [← meromorphicNFAt_toMeromorphicNFAt.meromorphicOrderAt_eq_zero_iff, hf]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
⊢ 0 ^ n = 0 ∨ g x = 0

Tactic:
left

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
⊢ 0 ^ n = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ 1 =ᶠ[𝓝[≠] x] fun z ↦ 1

Tactic:
exact eventuallyEq_nhdsWithin_of_eqOn fun _ ↦ congrFun rfl

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
y : 𝕜
a✝ : y ∈ Finite.toFinset h✝
h : x = y
⊢ ‖(x - y) ^ update d x 0 y‖ ≠ 0

Tactic:
rw [h]
      simp_all

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ AnalyticOnNhd 𝕜 g U

pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ (u : ↑U), g ↑u ≠ 0

pp: case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
· -- AnalyticOnNhd 𝕜 g U
    rw [← hg.divisor_nonneg_iff_analyticOnNhd, divisor_of_toMeromorphicNFOn (hφ.inv.smul h₁f),
      divisor_smul hφ.inv h₁f _ (fun z hz ↦ h₂f ⟨z, hz⟩), divisor_inv,
      Function.FactorizedRational.divisor h₃f, neg_add_cancel]
    intro z hz
    simpa [meromorphicOrderAt_inv] using meromorphicOrderAt_ne_top (divisor f U)

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ (u : ↑U), g ↑u ≠ 0

case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ meromorphicOrderAt g u = 0

Tactic:
← meromorphicOrderAt_congr
        (toMeromorphicNFOn_eq_self_on_nhdsNE (hφ.inv.smul h₁f) hu).symm,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ meromorphicOrderAt (φ⁻¹ • f) u = 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz : ¬z ∉ U
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z

Tactic:
by_cases hz : z ∈ F.support

Goal state after:
case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z

case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ meromorphicOrderAt (f * g⁻¹) x = meromorphicOrderAt f x - meromorphicOrderAt g x

Tactic:
meromorphicOrderAt_mul hf hg.inv,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ meromorphicOrderAt f x + meromorphicOrderAt g⁻¹ x = meromorphicOrderAt f x - meromorphicOrderAt g x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
x✝ : Set ↑U
| x✝ ⊆ {u | meromorphicOrderAt f ↑u = ⊤} ∧ IsOpen[instTopologicalSpaceSubtype] x✝ ∧ z ∈ x✝

Tactic:
left

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
x✝ : Set ↑U
| x✝ ⊆ {u | meromorphicOrderAt f ↑u = ⊤}