mathlib-initiative/mathlib-tactics huggingface dataset:
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
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

Tactic:
rw [WithTop.coe_lt_coe] at h

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
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
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : 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₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤

Goal state after:
case pos
𝕜 : 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₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

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₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : 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
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

Tactic:
by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤

Goal state after:
case pos
𝕜 : 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₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

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₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe
𝕜 : 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
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
have : (0 : E) = (x - x) ^ n • g x := by
      have : 0 < n := by simpa [h'o] using ho
      simp [zero_pow_eq_zero.2 this.ne']

Goal state after:
case coe
𝕜 : 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 = (x - x) ^ n • g x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicOrderAt f₂ x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff] at h₁f₁ ⊢

Goal state after:
case pos.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z = ↑(d z)

Tactic:
rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ ∃ g,
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧ ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ, (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z_1 = (z_1 - z) ^ d z • g z_1
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
nneg : 0 ≤ meromorphicOrderAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g

pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
g : 𝕜 → E
hg₁ : AnalyticAt 𝕜 g x
hg₂ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
· cases h₀ : meromorphicOrderAt f x with
    | top => exact ⟨0, analyticAt_const, meromorphicOrderAt_eq_top_iff.mp h₀⟩
    | coe n =>
      obtain ⟨g, hg, -, hfg⟩ := (meromorphicOrderAt_eq_int_iff hf).mp h₀
      refine ⟨fun z ↦ (z - x) ^ n • g z, ?_, hfg⟩
      exact (AnalyticAt.zpow_nonneg (by fun_prop) (by simpa [h₀] using nneg)).smul hg

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
g : 𝕜 → E
hg₁ : AnalyticAt 𝕜 g x
hg₂ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt f x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
h_num_ne_zero : ↑R ^ 2 - (starRingEnd ℂ) w * z ≠ 0
⊢ canonicalFactor R w z ≠ 0

Tactic:
canonicalFactor_apply

Goal state after:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
h_num_ne_zero : ↑R ^ 2 - (starRingEnd ℂ) w * z ≠ 0
⊢ (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w)) ≠ 0
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_cases h₂f₁ : meromorphicOrderAt f₁ x = ⊤

Goal state after:
case pos
𝕜 : 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
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

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
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
this : ∀ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x ≠ 0
⊢ log ((∏ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x) * ‖g z‖) =
    ((∑ i ∈ h₃f.toFinset, fun x ↦ ↑(D i) * log ‖x - i‖) + fun x ↦ log ‖g x‖) z

Tactic:
log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]),

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
this : ∀ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x ≠ 0
⊢ log (∏ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x) + log ‖g z‖ =
    ((∑ i ∈ h₃f.toFinset, fun x ↦ ↑(D i) * log ‖x - i‖) + fun x ↦ log ‖g x‖) z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
this✝ : x ∉ sphere 0 R
this : meromorphicOrderAt g x = 0
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
rw [divisor_apply D.meromorphicNFOn.meromorphicOn (mem_closedBall_zero_iff.mpr h.le)]

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
this✝ : x ∉ sphere 0 R
this : meromorphicOrderAt g x = 0
⊢ (meromorphicOrderAt g x).untop₀ = (divisor f (sphere 0 R)) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : R < ‖x‖
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
have : x ∉ sphere (0 : ℂ) R := by aesop
    simp_all

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
g : ℂ → E
D : CanonicalDecomp f g R
h₄g : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤
h : ℂ → E
h₁h : AnalyticOnNhd ℂ h (closedBall 0 R)
h₂h : ∀ (u : ↑(closedBall 0 R)), h ↑u ≠ 0
h₃h : g =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h
a : ℂ
h₁a : f a = ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g) a
h₂a : g a = ((∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h) a
⊢ f a =
    (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
          ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor g (closedBall 0 R)) v) •
        h)
      a

Tactic:
simp_all [← smul_assoc]

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

Goal state before:
pp: case refine_2
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
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
⊢ Γ 1 = Γ' 1

Tactic:
rw [(cov.eq_liftPath_iff' <| by simp [γ_0, he]).mpr ⟨Γ_lifts, Γ_0⟩,
    (cov.eq_liftPath_iff' <| by simp [γ'_0, he]).mpr ⟨Γ'_lifts, Γ'_0⟩]

Goal state after:
case refine_2
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
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
⊢ (cov.liftPath (f.comp γ) e₀ ⋯) 1 = (cov.liftPath (f.comp γ') e₀ ⋯) 1
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
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
F' : C(A, E)
hF'₁ : F' a₀ = ↑(F a₀)
hF'₂ : ∀ (x : A), p (F' x) = ↑(f x)
a : A
⊢ p (F' a) ∈ s

Tactic:
hF'₂

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
F' : C(A, E)
hF'₁ : F' a₀ = ↑(F a₀)
hF'₂ : ∀ (x : A), p (F' x) = ↑(f x)
a : A
⊢ ↑(f a) ∈ s
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : 0 < sSupNormIm f 0 ∧ 0 < sSupNormIm f 1
⊢ interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Tactic:
exact interpStrip_eq_of_pos f z h.1 h.2

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Tactic:
by
  by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
  · rw [interpStrip_eq_of_zero _ z h]
    rcases h with h0 | h1
    · simp only [h0, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ne_eq, true_and, ofReal_eq_zero]
      left
      rw [sub_eq_zero, eq_comm]
      simp only [Complex.ext_iff, one_re, ne_of_lt hz.2, false_and, not_false_eq_true]
    · simp only [h1, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq, true_and]
      right
      rw [eq_comm]
      simp only [Complex.ext_iff, zero_re, ne_of_lt hz.1, false_and, not_false_eq_true]
  · replace h : (0 < sSupNormIm f 0) ∧ (0 < sSupNormIm f 1) :=
      ⟨(lt_of_le_of_ne (sSupNormIm_nonneg f 0) (ne_comm.mp h.1)),
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) (ne_comm.mp h.2))⟩
    exact interpStrip_eq_of_pos f z h.1 h.2

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

Goal state before:
pp: case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re - l ≤ u - l

Tactic:
sub_le_sub_iff_right l

Goal state after:
case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re ≤ u
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x) = ∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)

Tactic:
have t₀ : Function.Periodic (fun w ↦ f (circleMap 0 1 w)) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
t₀ : Function.Periodic (fun w ↦ f (circleMap 0 1 w)) (2 * π)
⊢ ∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x) = ∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (⇑L ∘ f) (circleMap c R θ) =
    L ((2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
rw [map_smul]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (⇑L ∘ f) (circleMap c R θ) =
    (2 * π)⁻¹ • L (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: a b : ℂ
⊢ (a + b).re * (a - b).re / ‖a - b‖ ^ 2 + (a + b).im * (a - b).im / ‖a - b‖ ^ 2 = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2

Tactic:
← add_div,

Goal state after:
a b : ℂ
⊢ ((a + b).re * (a - b).re + (a + b).im * (a - b).im) / ‖a - b‖ ^ 2 = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
⊢ ContinuousAt (fun x ↦ x * log x) x

Tactic:
obtain hx | rfl := ne_or_eq x 0

Goal state after:
case inl
x : ℝ
hx : x ≠ 0
⊢ ContinuousAt (fun x ↦ x * log x) x

case inr
⊢ ContinuousAt (fun x ↦ x * log x) 0
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case neg
n : ℕ
x : ℝ
hn : ¬n = 0
hx : 1 < |x|
⊢ log⁺ (x ^ n) = ↑n * log⁺ x

Tactic:
have : 1 ≤ |x ^ n| := by simp_all [one_le_pow₀, hx.le]

Goal state after:
case neg
n : ℕ
x : ℝ
hn : ¬n = 0
hx : 1 < |x|
this : 1 ≤ |x ^ n|
⊢ log⁺ (x ^ n) = ↑n * log⁺ x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Tactic:
rcases le_or_gt a b with hab | hab
  · calc
      ∫ x in Ι a b, |x - a| ^ n = ∫ x in a..b, |x - a| ^ n := by
        rw [uIoc_of_le hab, ← integral_of_le hab]
      _ = ∫ x in 0..(b - a), x ^ n := by
        simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
        refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl
        rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
        exact hx.1
      _ = |b - a| ^ (n + 1) / (n + 1) := by simp [abs_of_nonneg (sub_nonneg.2 hab)]
  · calc
      ∫ x in Ι a b, |x - a| ^ n = ∫ x in b..a, |x - a| ^ n := by
        rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]
      _ = ∫ x in b - a..0, (-x) ^ n := by
        simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
        refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl
        rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
        exact hx.2
      _ = |b - a| ^ (n + 1) / (n + 1) := by
        simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]

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

Goal state before:
pp: case inl
b : ℝ
h : b < 0
⊢ ∫ (t : ℝ) in 0..b, log (-t) = b * log b - b

Tactic:
intervalIntegral.integral_comp_neg,

Goal state after:
case inl
b : ℝ
h : b < 0
⊢ ∫ (x : ℝ) in -b..-0, log x = b * log b - b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
by
  have : ∀ x s : ℝ, (((↑1 + x ^ 2) ^ s : ℝ) : ℂ) = (1 + (x : ℂ) ^ 2) ^ (s : ℂ) := by
    intro x s
    norm_cast
    rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
    exact add_nonneg zero_le_one (sq_nonneg x)
  rw [← ofReal_inj]
  convert! integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)
  · rw [← intervalIntegral.integral_ofReal]
    congr with x : 1
    rw [ofReal_mul, this x t]
  · simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)]
    push_cast; rfl
  · rw [← ofReal_one, ← ofReal_neg, Ne, ofReal_inj]
    exact ht

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_zer : I∞.ZeroAtFilter f
⊢ cuspFunction h f 0 = 0

Tactic:
by
  simpa only [cuspFunction, update_self] using (h_zer.comp (invQParam_tendsto hh)).limUnder_eq

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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
t₀ : c ∈ CB
⊢ AccPt c (𝓟 CB)

Tactic:
apply accPt_iff_frequently_nhdsNE.mpr

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := ⋯
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
t₀ : c ∈ CB
⊢ ∃ᶠ (y : ℂ) in 𝓝[≠] c, y ∈ CB
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.discr = A.trace ^ 2 - 4 * A.det

Tactic:
rw [discr, Polynomial.discr_of_degree_eq_two (by simp; norm_cast)]

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.charpoly.coeff 1 ^ 2 - 4 * A.charpoly.coeff 0 * A.charpoly.coeff 2 = A.trace ^ 2 - 4 * A.det