mathlib-initiative/mathlib-tactics huggingface dataset:
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₁)
⊢ ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)

Tactic:
refine norm_le_of_forall_mem_frontier_norm_le isBounded_ball (hdg'.diffContOnCl_ball subset_rfl)
    ?_ ?_

Goal state after:
case inr.refine_1
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₁)
⊢ ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)

case inr.refine_2
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₁)
⊢ z ∈ closure (ball c R₁)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f ((lineMap c z) 0)) =o[𝓝 ((lineMap c z) 0)] fun w ↦ ‖w - (lineMap c z) 0‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Tendsto (⇑(lineMap c z)) (𝓝 0) (𝓝 ((lineMap c z) 0))

Tactic:
exact Continuous.tendsto (by fun_prop) 0

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
hf : ¬MeromorphicOn f U
⊢ (divisor f U) z = 0

Tactic:
unfold divisor
  aesop

Goal state after:
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
hf₁ : MeromorphicOn f₁ U
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ (U \ {x | f₁ x = f₂ x})ᶜ
⊢ f₁ a = f₂ a

Tactic:
simp at ha

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ U → f₁ a = f₂ a
⊢ f₁ a = f₂ a
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 : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ 0 ≤ divisor f U

Tactic:
by
  intro x
  by_cases hx : x ∈ U
  · simp [hf.meromorphicOn, hx, (hf x hx).meromorphicOrderAt_nonneg]
  simp [hx]

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

Goal state before:
pp: case mpr.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : AnalyticAt 𝕜 f x
⊢ MeromorphicNFAt f x

pp: case mpr.inr
𝕜 : 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 < 0
h₃ : f x = 0
⊢ MeromorphicNFAt f x

Tactic:
· by_cases h₂f : analyticOrderAt f x = ⊤
      · rw [analyticOrderAt_eq_top] at h₂f
        tauto
      · right
        use analyticOrderNatAt f x
        have : analyticOrderAt f x ≠ ⊤ := h₂f
        rw [← ENat.natCast_toNat_eq_self, eq_comm, h.analyticOrderAt_eq_natCast] at this
        obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
        use g, h₁g, h₂g
        simpa

Goal state after:
case mpr.inr
𝕜 : 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 < 0
h₃ : f x = 0
⊢ MeromorphicNFAt f x
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
x : 𝕜
h : AnalyticAt 𝕜 f x
⊢ MeromorphicAt f x

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicAt f x

Tactic:
· exact h.meromorphicAt

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicAt f x
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
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ Tendsto ((fun x_1 ↦ x_1 - x) ^ (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x) (𝓝 (meromorphicTrailingCoeffAt f x))

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h).1 h₂

Goal state after:
case neg
𝕜 : 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
⊢ Tendsto ((fun x_1 ↦ x_1 - x) ^ (-(meromorphicOrderAt f x).untop₀) • 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 : 𝕜
ho : meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
have hf : MeromorphicAt f x := meromorphicAt_of_meromorphicOrderAt_ne_zero ho.ne
  simp only [← tendsto_norm_atTop_iff_cobounded]
  obtain ⟨m, hm⟩ := WithTop.ne_top_iff_exists.mp ho.ne_top
  have m_neg : m < 0 := by simpa [← hm] using ho
  rcases (meromorphicOrderAt_eq_int_iff hf).1 hm.symm with ⟨g, g_an, gx, hg⟩
  have A : Tendsto (fun z ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop := by
    simp only [norm_smul]
    apply Filter.Tendsto.atTop_mul_pos (C := ‖g x‖) (by simp [gx]) _
      g_an.continuousAt.continuousWithinAt.tendsto.norm
    have : Tendsto (fun z ↦ z - x) (𝓝[≠] x) (𝓝[≠] 0) := by
      refine tendsto_nhdsWithin_iff.2 ⟨?_, ?_⟩
      · have : ContinuousWithinAt (fun z ↦ z - x) {x}ᶜ x := by fun_prop
        simpa using this.tendsto
      · filter_upwards [self_mem_nhdsWithin] with y hy
        simpa [sub_eq_zero] using hy
    exact (tendsto_norm_cobounded_atTop.comp (tendsto_zpow_nhdsNE_zero_cobounded m_neg)).comp this
  apply A.congr'
  filter_upwards [hg] with z hz using by simp [hz]

Goal state after:
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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = ↑↑n
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ ↑n • g z
this : 0 < n
⊢ 0 = (x - x) ^ n • g x

Tactic:
simp [zero_pow_eq_zero.2 this.ne']

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

Goal state before:
pp: case inr
𝕜 : 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
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ False

Tactic:
rcases ho.lt_or_gt with ho | ho

Goal state after:
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
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
⊢ False

case inr.inr
𝕜 : 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
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : 0 < meromorphicOrderAt f x
⊢ False
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = ⊤

pp: case neg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : ¬e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = 0

Tactic:
· simp [he, meromorphicOrderAt_eq_top_iff]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : ¬e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
y : 𝕜
hy : f y = 0
⊢ (f ^ n) y = 0

Tactic:
simp [hy, zero_zpow n hn]

Goal state after:
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
by
  -- Handle the trivial cases where one of the orders equals ⊤
  by_cases h₂f₁ : meromorphicOrderAt f₁ x = ⊤
  · rw [h₂f₁, min_top_left, meromorphicOrderAt_congr]
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₂f₁]
    simp
  by_cases h₂f₂ : meromorphicOrderAt f₂ x = ⊤
  · simp only [h₂f₂, le_top, inf_of_le_left]
    rw [meromorphicOrderAt_congr]
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₂f₂]
    simp
  -- General case
  lift meromorphicOrderAt f₁ x to ℤ using h₂f₁ with n₁ hn₁
  lift meromorphicOrderAt f₂ x to ℤ using h₂f₂ with n₂ hn₂
  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn₁.symm
  obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm
  let n := min n₁ n₂
  let g := (fun z ↦ (z - x) ^ (n₁ - n)) • g₁ + (fun z ↦ (z - x) ^ (n₂ - n)) • g₂
  have h₁g : AnalyticAt 𝕜 g x := by
    apply AnalyticAt.add
    · apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_left n₁ n₂))).smul h₁g₁
    apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_right n₁ n₂))).smul h₁g₂
  have : f₁ + f₂ =ᶠ[𝓝[≠] x] ((· - x) ^ n) • g := by
    filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]
    simp_all [g, ← smul_assoc, ← zpow_add', sub_ne_zero]
  have t₀ : MeromorphicAt ((· - x) ^ n) x := by fun_prop
  have t₁ : meromorphicOrderAt ((· - x) ^ n) x = n :=
    (meromorphicOrderAt_eq_int_iff t₀).2 ⟨1, analyticAt_const, by simp⟩
  rw [meromorphicOrderAt_congr this, meromorphicOrderAt_smul t₀ h₁g.meromorphicAt, t₁]
  exact le_add_of_nonneg_right h₁g.meromorphicOrderAt_nonneg

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

Goal state before:
pp: a : Circle
⊢ 1 = ↑1

Tactic:
Units.val_one

Goal state after:
a : Circle
⊢ 1 = 1
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
⊢ {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤} ∈ codiscrete ↑U

Tactic:
rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin]

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
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤}))
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
⊢ (p ∘ fun ta ↦
      (cov.liftPath (H.comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) ta.2))) (f ta.2) ⋯) ta.1) =
    ⇑H

Tactic:
ext ⟨t, a⟩; exact congr_fun (cov.liftPath_lifts ..) t

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

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
a : A
⊢ Continuous[_, inst✝²] fun x ↦
    (cov.liftPath (H.comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (x, a).2))) (f (x, a).2) ⋯) (x, a).1

Tactic:
by dsimp only; exact (cov.liftPath (γ_0 := by simp [*])).2

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

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
X✝ Y✝ Z✝ : FundamentalGroupoid X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾cov.monodromy (x✝¹ ≫ x✝) = ↾cov.monodromy x✝¹ ≫ ↾cov.monodromy x✝

Tactic:
by ext : 3; simpa using! cov.monodromy_trans_apply _ _ _

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
Γ : Path.Homotopic.Quotient ↑e ↑(⋯.monodromy γ e) := ⋯.liftPathQuotient γ e
g' : C(E, E) := { toFun := fun x ↦ g • x, continuous_toFun := ⋯ }
p' : C(E, X) := { toFun := p, continuous_toFun := ⋯ }
hgp : p'.comp g' = p'
⊢ Γ.map (p'.comp g') = γ.cast ⋯ ⋯

Tactic:
convert hp.isCoveringMap.map_liftPathQuotient γ e using 2

Goal state after:
case e'_1.e'_3
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
Γ : Path.Homotopic.Quotient ↑e ↑(⋯.monodromy γ e) := ⋯.liftPathQuotient γ e
g' : C(E, E) := { toFun := fun x ↦ g • x, continuous_toFun := ⋯ }
p' : C(E, X) := { toFun := p, continuous_toFun := ⋯ }
hgp : p'.comp g' = p'
⊢ p' (g' ↑e) = { toFun := p, continuous_toFun := ⋯ } ↑e

case e'_1.e'_4
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
Γ : Path.Homotopic.Quotient ↑e ↑(⋯.monodromy γ e) := ⋯.liftPathQuotient γ e
g' : C(E, E) := { toFun := fun x ↦ g • x, continuous_toFun := ⋯ }
p' : C(E, X) := { toFun := p, continuous_toFun := ⋯ }
hgp : p'.comp g' = p'
⊢ p' (g' ↑(⋯.monodromy γ e)) = { toFun := p, continuous_toFun := ⋯ } ↑(⋯.monodromy γ e)

case e'_3
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
Γ : Path.Homotopic.Quotient ↑e ↑(⋯.monodromy γ e) := ⋯.liftPathQuotient γ e
g' : C(E, E) := { toFun := fun x ↦ g • x, continuous_toFun := ⋯ }
p' : C(E, X) := { toFun := p, continuous_toFun := ⋯ }
hgp : p'.comp g' = p'
e_1✝ :
  Path.Homotopic.Quotient (p' (g' ↑e)) (p' (g' ↑(⋯.monodromy γ e))) =
    Path.Homotopic.Quotient ({ toFun := p, continuous_toFun := ⋯ } ↑e)
      ({ toFun := p, continuous_toFun := ⋯ } ↑(⋯.monodromy γ e))
⊢ γ.cast ⋯ ⋯ ≍ γ.cast ⋯ ⋯
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case mp
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
γ : FundamentalGroup X x
h : γ ∈ (⋯.monodromyPerm x).ker
⊢ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯) ((⋯.liftPathQuotient γ e).cast ⋯ ⋯) = γ

Tactic:
FundamentalGroup.mapOfEq_apply,

Goal state after:
case mp
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
γ : FundamentalGroup X x
h : γ ∈ (⋯.monodromyPerm x).ker
⊢ (((⋯.liftPathQuotient γ e).cast ⋯ ⋯).map { toFun := p, continuous_toFun := ⋯ }).cast ⋯ ⋯ = γ
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: x : ℝ
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
⊢ deriv (fun x ↦ (log x)⁻¹) x = -x⁻¹ / log x ^ 2

Tactic:
have := mt (continuousAt (𝕜 := ℝ)) not_continuousAt_inv_log_one

Goal state after:
x : ℝ
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
⊢ deriv (fun x ↦ (log x)⁻¹) x = -x⁻¹ / log x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)

Tactic:
by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv.refine_1.inl
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : c ≤ 0
⊢ x ≠ 0

Tactic:
rw [max_eq_left hc] at hx; exact hx.2.ne

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)

Tactic:
rcases hexp with ⟨c, hc, B, hO⟩
    refine ⟨c, hc, B, .trans (.of_bound' ?_) hO⟩
    refine eventually_inf_principal.2 <| Eventually.of_forall fun z hz => ?_
    rw [hgn]
    refine mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 ?_)
    exact mul_nonpos_of_nonpos_of_nonneg ε₀.le (le_of_lt hz)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b ^ ↑(r + 1)).re - (↑a ^ ↑(r + 1)).re)

Tactic:
rpow_def

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = circleAverage (fun x ↦ log ‖1 - x⁻¹ * a‖) 0 1

Tactic:
by
    apply circleAverage_congr_sphere
    intro z hz
    simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
    congr 1
    have : z ≠ 0 := fun h ↦ by simp [h] at hz
    calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a

Tactic:
simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using
    integral_deriv_mul_eq_sub (fun x _ => hasDerivAt_sin x) (fun x _ => hasDerivAt_cos x)
      continuousOn_cos.intervalIntegrable continuousOn_sin.neg.intervalIntegrable

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ ↑R * z + c - a = ↑R * (z + (↑R)⁻¹ * (c - a))

Tactic:
field [Complex.ofReal_ne_zero.mpr hR]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case h
a c : ℂ
R : ℝ
z z₁ z₂ : ℂ
hR : ¬R = 0
hz : ‖z‖ = 1
hz₁ : ‖z₁‖ = 1 ∧ z₁ + (↑R)⁻¹ * (c - a) = 0
hz₂ : ‖z₂‖ = 1 ∧ z₂ + (↑R)⁻¹ * (c - a) = 0
⊢ z₁ = z₂

Tactic:
rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]

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

Goal state before:
pp: case h
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, y ∈ {0}ᶜ → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
y : ℝ
q : ℂ
⊢ q ∈ S → q ∉ {0} → (norm ∘ cuspFunction h f) q = y → y ≤ c

Tactic:
hq

Goal state after:
case h
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, y ∈ {0}ᶜ → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
y : ℝ
q : ℂ
hq : q ∈ S
⊢ q ∉ {0} → (norm ∘ cuspFunction h f) q = y → y ≤ c
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
this : Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))
⊢ Tendsto f I∞ (𝓝 (cuspFunction h f 0))

Tactic:
by
    simpa only [Function.comp_def, eq_cuspFunction hh.ne' hf] using this.comp (qParam_tendsto hh)

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case neg
a : ℂ
h : a.im < 0
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

Tactic:
simp only [re_add_im, ↓reduceIte, h.not_ge, neg_one_mul, ← ofReal_neg,
    ← cpow_inv_two_im_eq_neg_sqrt h]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ sqrt I = ↑√2⁻¹ * (1 - I) * I

Tactic:
rw [sqrt_eq_ite]
  split_ifs with h
  · simp_rw [RingEquiv.symm_apply_eq, map_mul]
    simp [h, mul_assoc, mul_add, add_comm, Complex.sqrt_I, add_mul]
  grind [I_eq_zero_or_im_I_eq_one]

Goal state after: