mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f a < deriv f b

pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ 0 ≤ deriv f b

Tactic:
· exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ 0 ≤ deriv f b
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ deriv f a < deriv f b

pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ 0 ≤ deriv f b

Tactic:
· exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ 0 ≤ deriv f b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
h : cos x = 0
this : ¬DifferentiableAt ℂ tan x
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
simp [deriv_zero_of_not_differentiableAt this, h, sq]

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

Goal state before:
pp: x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
simp [deriv_zero_of_not_differentiableAt this, h, sq]

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

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

Tactic:
have hy : 0 < y := by
    have := mul_pos_iff.mp (zero_lt_one.trans h)
    simpa [hx, hx.asymm]

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

Goal state before:
pp: case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
hys' : y ∈ interior S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hys'

Goal state after:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
hys' : ∃ l u, y ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
suffices ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1) by
    have hz' : ‖z - c‖ ≠ 0 := by simpa [sub_eq_zero] using hne
    simpa [g', hne, g, div_pow, mul_comm, field] using this

Goal state after:
case inr
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ normSq ↑z < 1

Tactic:
← Complex.norm_mul_self_eq_normSq,

Goal state after:
z : 𝔻
⊢ ‖↑z‖ * ‖↑z‖ < 1
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝕔𝔻
⊢ normSq ↑z ≤ 1

Tactic:
← Complex.norm_mul_self_eq_normSq,

Goal state after:
z : 𝕔𝔻
⊢ ‖↑z‖ * ‖↑z‖ ≤ 1
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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₁
⊢ f z = (fun z ↦ f c + (z - c) • dslope f c z₀) z

Tactic:
have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩

Goal state after:
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₁
⊢ f z = (fun z ↦ f c + (z - c) • dslope f c z₀) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : 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
⊢ divisor f₁ U = divisor f₂ U

Tactic:
by
  by_cases hf₁ : MeromorphicOn f₁ U
  · 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]
  · simp [divisor, hf₁, (meromorphicOn_congr_codiscreteWithin h₁ h₂).not.1 hf₁]

Goal state after:
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:
by
  constructor
  · intro h
    have t₀ := meromorphicOrderAt_congr h
    by_cases cs : meromorphicOrderAt f x = 0
    · rw [cs] at t₀
      have Z := (hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq cs.symm)).continuousAt
      have W := (hg.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq t₀)).continuousAt
      exact (Z.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE W).1 h
    · apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE h
      let h₁f := cs
      rw [hf.meromorphicOrderAt_eq_zero_iff] at h₁f
      let h₁g := cs
      rw [t₀, hg.meromorphicOrderAt_eq_zero_iff] at h₁g
      simp only [not_not] at *
      rw [h₁f, h₁g]
  · exact (Filter.EventuallyEq.filter_mono · nhdsWithin_le_nhds)

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
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ (meromorphicOrderAt (f ∘ fun x ↦ x + c) (x - c)).untop₀ = (divisor f (U + {c})) x

pp: case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn (f ∘ fun x ↦ x + c) U

pp: case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x - c ∈ U

Tactic:
divisor_apply

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ (meromorphicOrderAt (f ∘ fun x ↦ x + c) (x - c)).untop₀ = (meromorphicOrderAt f x).untop₀

case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn f (U + {c})

case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x ∈ U + {c}

case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn (f ∘ fun x ↦ x + c) U

case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x - c ∈ U
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt f x = g x

Tactic:
simp only [h₃, WithTop.untop₀_top, zpow_zero, one_smul,
      MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top] at ⊢ h
    apply EventuallyEq.eq_of_nhds (f := 0)
    rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) (by fun_prop)]
    apply (h.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₃)).symm

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
⊢ MeromorphicNFAt (f / g) x

Tactic:
by
  rw [div_eq_mul_inv]
  rcases hor with hgne | hfne
  · have hf := hf.meromorphicNFAt
    have hgAnalytic : AnalyticAt 𝕜 g x := by grind [meromorphicNFAt_iff_analyticAt_or]
    have hgInvAnalytic : AnalyticAt 𝕜 g⁻¹ x := hgAnalytic.inv hgne
    rwa [← meromorphicNFAt_mul_iff_left hgInvAnalytic (inv_ne_zero hgne)] at hf
  · grind [meromorphicNFAt_mul_iff_right, hg.inv]

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
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
hf : ¬MeromorphicAt f x
⊢ toMeromorphicNFAt f x =ᶠ[𝓝 x] toMeromorphicNFAt g x

Tactic:
simp [hf, MeromorphicAt.meromorphicAt_congr hfg |>.not.mp]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₁ x < ↑n₂
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x

Tactic:
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₁ x < ↑n₂
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ 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
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : (z - x) ^ Exists.choose hf • f z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
hz : z ∈ {x}ᶜ
⊢ g z = 0

Tactic:
rwa [hfz_eq hz, ← mul_smul, smul_eq_zero_iff_right] at hfz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : ((z - x) ^ Exists.choose hf * (z - x) ^ n) • g z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
hz : z ∈ {x}ᶜ
⊢ (z - x) ^ Exists.choose hf * (z - x) ^ n ≠ 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 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
⊢ n = 0

Tactic:
h₃f

Goal state after:
𝕜 : 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 : 0 = ↑n
h₃f : meromorphicOrderAt f x = 0
⊢ n = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h₁f₁ : ¬↑n₁ = ⊤
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h₁ : ↑n₁ = ↑n₂
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h₁f₁ : ¬↑n₁ = ⊤
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h₁ : ↑n₁ = ↑n₂
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
c : E
c_ne : c ≠ 0
h'c : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ c = 0

Tactic:
exact tendsto_nhds_unique h'c hc

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
⊢ ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u = (fun x ↦ x - u₀) ^ d u₀ * ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d u₀ 0 u

Tactic:
have : (fun u ↦ (fun x ↦ x - u) ^ d u).mulSupport ⊆ hd.toFinset := by
      simp [mulSupport]
    rw [finprod_eq_prod_of_mulSupport_subset _ this]
    have : u₀ ∈ hd.toFinset := by simp_all
    rw [← Finset.mul_prod_erase hd.toFinset _ this]
    congr 1
    have : (fun u ↦ (· - u) ^ (update d u₀ 0 u)).mulSupport ⊆ hd.toFinset.erase u₀ := by
      rw [mulSupport]
      intro x hx
      by_cases h₁x : x = u₀ <;> simp_all
    simp_all [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]

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

Goal state before:
pp: R : ℝ
w : ℂ
⊢ canonicalFactor R w w = 0

Tactic:
simp [canonicalFactor_apply]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
⊢ min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
Module: Mathlib.Analysis.Meromorphic.Order

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

Tactic:
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt : MeromorphicAt f₂ x → ↑n₁ < ↑n₂ → meromorphicOrderAt (f₁ + f₂) x = ↑n₁
h : ↑n₁ < ↑n₂
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ meromorphicOrderAt (f₁ + f₂) x = ↑n₁
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a : Circle
⊢ rotation a ≠ conjLIE

Tactic:
intro h
  have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
  have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
  rw [rotation_apply, map_one, mul_one] at h1
  rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI
  exact one_ne_zero hI

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g

Tactic:
· rw [finprod_eq_prod_of_mulSupport_subset_of_finite _ (by aesop) η₀]
        filter_upwards [toMeromorphicNFOn_eqOn_codiscrete hφ] using by simp_all [g]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝¹ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
x✝ : ↑I
h : x✝ ∈ Set.Icc 0 (t (n + 1)) ∩ closure {a | a ≤ t n}
⊢ x✝ ∈ Set.Icc 0 (t n)

Tactic:
rw [closure_le_eq continuous_id' continuous_const] at h; exact ⟨h.1.1, h.2⟩

Goal state after: