mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x - y‖ = ‖x‖ + ‖y‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
    norm_sub_pow_two_real, inner_eq_neg_mul_norm_of_angle_eq_pi h]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x‖ ^ 2 - 2 * -(‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
Module: Mathlib.Analysis.Complex.CoveringMap

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

Tactic:
have (x : 𝕜) : x ^ n = 0 ↔ x = 0 := zpow_eq_zero_iff (by aesop)
  refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
  · convert isClosed_singleton (x := (0 : 𝕜)).isOpen_compl
    ext; simp [this]
  · convert! (isCoveringMap_zpow n hn).comp_homeomorph (.setCongr _) using 1
    ext; simpa using! (this _).not

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

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

Tactic:
exact isQuotientCoveringMap_npow n (by aesop) (by simpa using surj)

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

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

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

Tactic:
· apply isOpen_setOfPred_eventually_nhdsWithin

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

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

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

Tactic:
· simp_all

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∉ U
⊢ min ((divisor f₁ U) z) ((divisor f₂ U) z) ≤ (divisor (f₁ + f₂) U) z

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
⊢ min ((divisor f₁ U) z) ((divisor f₂ U) z) ≤ (divisor (f₁ + f₂) U) z

Tactic:
· simp_all

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
⊢ min ((divisor f₁ U) z) ((divisor f₂ U) z) ≤ (divisor (f₁ + f₂) U) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
· simp_all

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
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
        rw [analyticAt_congr h₃g]
        apply (AnalyticAt.zpow_nonneg (by fun_prop) hn).smul h₁g

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : meromorphicOrderAt f₂ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
· simp_all

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
hz : z ∈ U
⊢ (divisor (f₁ • f₂) U) z = (divisor f₁ U + divisor f₂ U) z

Tactic:
lift meromorphicOrderAt f₁ z to ℤ using (h₂f₁ z hz) with a₁ ha₁

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
hz : z ∈ U
a₁ : ℤ
ha₁ : ↑a₁ = meromorphicOrderAt f₁ z
⊢ (divisor (f₁ • f₂) U) z = (divisor f₁ U + divisor f₂ U) z
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
· obtain ⟨m, g, h₁g, h₂g, h₃g⟩ := hf
    right
    use n * m, g ^ n, h₁g.zpow h₂g
    constructor
    · rw [Pi.pow_apply]
      exact zpow_ne_zero n h₂g
    · filter_upwards [h₃g] with z hz
      simp [hz, mul_zpow, (zpow_mul' (z - x) n m).symm]

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

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

Tactic:
exact hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₂f)

Goal state after:
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
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 : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ g x = 0

Tactic:
apply EventuallyEq.eq_of_nhds

Goal state after:
case pos
𝕜 : 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 : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ g =ᶠ[𝓝 x] fun {x} ↦ 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn (g • f) U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (g • f) z

Tactic:
exact h hz

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : ¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
· simp_all

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

Tactic:
rw [h₁]

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ x ∉ ↑h.toFinset → (x - x) ^ update d x 0 x = 1
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : ¬u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

Tactic:
· simp_all

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
⊢ ∏ i ∈ Finite.toFinset h₁, (x - i) ^ update d x 0 i = ∏ᶠ (u : 𝕜), (x - u) ^ d u

Tactic:
have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport fun u ↦ (x - u) ^ d u) ⊆ ↑(Finite.toFinset h₁)
⊢ ∏ i ∈ Finite.toFinset h₁, (x - i) ^ update d x 0 i = ∏ᶠ (u : 𝕜), (x - u) ^ d u
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case mpr
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ z = w → canonicalFactor R w z = 0

Tactic:
· simp_all

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

Goal state before:
pp: case pos
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
MeromorphicOn.divisor_apply
      (fun z hz ↦ meromorphic_canonicalFactor R w z) hz

Goal state after:
case pos
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∉ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
· simp_all

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

Goal state before:
pp: case hy
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ ‖g x‖ ≠ 0

Tactic:
· simp_all

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

Goal state before:
pp: case neg
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
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
a : ℂ
ha : a ∉ ball 0 R
⊢ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x ≠ 0

Tactic:
· simp_all

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
cov : IsCoveringMap p
x y z : X
γ : Path.Homotopic.Quotient x y
γ' : Path.Homotopic.Quotient y z
e : ↑(p ⁻¹' {x})
⊢ cov.monodromy (γ.trans γ') e = cov.monodromy γ' (cov.monodromy γ e)

Tactic:
obtain ⟨γ⟩ := γ; obtain ⟨γ'⟩ := γ'
  exact Subtype.ext (congr($(cov.liftPath_trans e.2.symm ..) 1).trans (Path.target _))

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
x c : 𝕜
f : 𝕜 → E
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + -c) x = meromorphicOrderAt f (x + -c)

Tactic:
← meromorphicOrderAt_comp_add_const_eq_meromorphicOrderAt

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
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯)) ⟨e₀, he⟩ = id ⟨e₀, he⟩

Tactic:
obtain ⟨⟨pΓΓ'⟩, eq⟩ := le ⟨fromPath (.mk pγγ'), rfl⟩

Goal state after:
case refine_2.mk
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
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
w✝ : FundamentalGroup E e₀
pΓΓ' : Path { as := e₀ }.as { as := e₀ }.as
eq :
  (mapOfEq { toFun := p, continuous_toFun := ⋯ } he)
      (Quot.mk (⇑(Path.Homotopic.setoid { as := e₀ }.as { as := e₀ }.as)) pΓΓ') =
    (FundamentalGroup.map f a₀) (fromPath (Path.Homotopic.Quotient.mk pγγ'))
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯)) ⟨e₀, he⟩ = id ⟨e₀, he⟩
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
⊢ log
      ‖((∏ i ∈ t₂, canonicalFactor R i w ^ (divisor f B₀R) i) * ∏ i ∈ t₁, (w - i) ^ (-divisor f S₀R) i) •
          meromorphicTrailingCoeffAt f w‖ =
    ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
have η₁ (x) (hx : x ∈ t₂) : ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0 := by
        refine zpow_ne_zero _ ?_
        rw [norm_ne_zero_iff]
        have h₁x : x ∈ ball 0 R := (divisor f B₀R).supportWithinDomain (ht₂ ▸ hx)
        refine canonicalFactor_ne_zero h₁x h₁w fun _ ↦ ?_
        simp_all [divisor_def, ← Finset.mem_coe]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
η₁ : ∀ x ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ log
      ‖((∏ i ∈ t₂, canonicalFactor R i w ^ (divisor f B₀R) i) * ∏ i ∈ t₁, (w - i) ^ (-divisor f S₀R) i) •
          meromorphicTrailingCoeffAt f w‖ =
    ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖
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
x : X
e : ↑(p ⁻¹' {x})
γ : FundamentalGroup X x
g : Gᵐᵒᵖ
⊢ (hp.fundamentalGroupToMulOpposite e) γ = g ↔ MulOpposite.unop g • ↑e = ↑(⋯.monodromy γ e)

Tactic:
fundamentalGroupToMulOpposite,

Goal state after:
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
g : Gᵐᵒᵖ
⊢ { toFun := fun γ ↦ MulOpposite.op ((hp.fiberEquivGroup e) (⋯.monodromy γ e)), map_one' := ⋯, map_mul' := ⋯ } γ = g ↔
    MulOpposite.unop g • ↑e = ↑(⋯.monodromy γ e)
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case hb₁
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ↑w.re + ↑z.im * I ∈ ball z (r - dist z c)

pp: case hb₂
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ↑w.re + ↑w.im * I ∈ ball z (r - dist z c)

Tactic:
· exact re_add_im_mul_mem_ball hw

Goal state after:
case hb₂
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ↑w.re + ↑w.im * I ∈ ball z (r - dist z c)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re))⁻¹ * ((ε + sSupNormIm f 1) ^ z.re)⁻¹ ≤ 1

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 1) ^ z.re

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)

Tactic:
← Real.rpow_neg_one,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re)) ^ (-1) * ((ε + sSupNormIm f 1) ^ z.re)⁻¹ ≤ 1

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 1) ^ z.re

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖

Tactic:
by
  simp only [norm_mul, ← ofReal_add, norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _,
    sub_re, one_re]
  rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀,
    ← Real.rpow_neg_one, ← Real.rpow_neg_one]
  · simp only [← Real.rpow_mul (le_of_lt (sSupNormIm_eps_pos f hε _)),
    mul_neg, mul_one, neg_sub, mul_assoc]
    simpa [F, norm_invInterpStrip _ _ hε, norm_smul, mul_comm] using
      norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip f ε hε z hd hB hz
  · simp only [Real.rpow_pos_of_pos (sSupNormIm_eps_pos f hε _) z.re]
  · simp only [Real.rpow_pos_of_pos (sSupNormIm_eps_pos f hε _) (1 - z.re)]

Goal state after: