mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
⊢ MeromorphicNFAt (f * g) x ↔ MeromorphicNFAt f x

Tactic:
rw [mul_comm, ← smul_eq_mul]
  exact meromorphicNFAt_smul_iff_right_of_analyticAt h₁g h₂g

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

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

Tactic:
h₂y

Goal state after:
𝕜 : 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 = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
⊢ y ∈ {x}ᶜ → ⋯.choose y = g y
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

Tactic:
h₂y,

Goal state after:
𝕜 : 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 = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
y : 𝕜
h₁y : (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ ⋯.choose y - g y = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

Tactic:
h₂y

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h₂f : ¬meromorphicOrderAt f x = ⊤
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
lift meromorphicOrderAt f x to ℤ using h₂f with n hn

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

Tactic:
h₂y

Goal state after:
𝕜 : 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 = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z
y : 𝕜
h₁y : f₁ y = (y - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ y
h₂y : f₂ y = (y - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ y
⊢ y ∈ {x}ᶜ → (f₁ • f₂) y = (y - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) y
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
⊢ ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x

Tactic:
intro τ

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
τ : ι
⊢ τ ∈ s₁ → MeromorphicAt (f τ) x
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
⊢ ((fun x ↦ x - z) ^ d z) x ≠ 0

Tactic:
simp only [Pi.pow_apply, ne_eq]

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
⊢ ¬(x - z) ^ d z = 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case h
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
⊢ meromorphicOrderAt (canonicalFactor R w) 0 ≠ ⊤

Tactic:
by_cases hw : w = 0

Goal state after:
case pos
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : w = 0
⊢ meromorphicOrderAt (canonicalFactor R w) 0 ≠ ⊤

case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ meromorphicOrderAt (canonicalFactor R w) 0 ≠ ⊤
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
w : ℂ
hw : w ∉ ball 0 R
⊢ MeromorphicNFOn (canonicalFactor R w ^ F w) (ball 0 R)

Tactic:
simp only [hw, not_false_eq_true, locallyFinsuppWithin.apply_eq_zero_of_notMem, zpow_zero]
      exact analyticOnNhd_const.meromorphicNFOn

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

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

Tactic:
simp only [h₁f, hu, divisor_apply]

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

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

Tactic:
← WithTop.coe_add

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

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ (p ∘ fun st ↦ (Γ st.2) st.1) = ⇑((↑γ).comp ContinuousMap.prodSwap)

pp: case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1

pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
· ext; apply Γ_lifts

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1

case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
· exact fun t ↦ (Γ t).2

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
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
⊢ AnalyticAt 𝕜 ((fun x_1 ↦ x_1 - x) ^ (n₂ - n₁)) x

Tactic:
apply AnalyticAt.zpow_nonneg (by fun_prop)
      (sub_nonneg.2 (le_of_lt (WithTop.coe_lt_coe.1 h)))

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

Goal state before:
pp: case pos
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
a : ℂ
ha : a ∈ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x

Tactic:
exact (analyticOnNhd_canonicalFactor _ _ _ (by aesop)).zpow
          (canonicalFactor_ne_zero ha (by aesop) (by aesop))

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 0

Tactic:
Function.comp_def,

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (fun x ↦ f (g x)) z = 0
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
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) ≠ ⊤
hr : meromorphicOrderAt f (g x) = ↑(meromorphicOrderAt f (g x)).untop₀
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

Tactic:
rw [meromorphicOrderAt_ne_top_iff hf] at hf'

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' :
  ∃ g_1,
    AnalyticAt 𝕜 g_1 (g x) ∧
      g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • g_1 z
hr : meromorphicOrderAt f (g x) = ↑(meromorphicOrderAt f (g x)).untop₀
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z ↦ expR (B * expR (c * |u z|))
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z ↦ expR (B * expR (c * |u z|))

Tactic:
have : ∀ {c₁ c₂ B₁ B₂}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ z,
      ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖ := fun hc hB₀ hB z ↦ by
    simp only [Real.norm_eq_abs, Real.abs_exp]; gcongr
  rcases hBf with ⟨cf, hcf, Bf, hOf⟩; rcases hBg with ⟨cg, hcg, Bg, hOg⟩
  refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩
  refine (hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)
  exacts [le_max_left _ _, le_max_left _ _, (le_max_left _ _).trans (le_max_right _ _),
    le_max_right _ _, le_max_left _ _, (le_max_right _ _).trans (le_max_right _ _)]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
⊢ canonicalCovariantTensor E = ∑ i, v i ⊗ₜ[ℝ] v i

Tactic:
by
  let w := stdOrthonormalBasis ℝ E
  calc ∑ m, w m ⊗ₜ[ℝ] w m
  _ = ∑ m, ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n := by
    congr 1 with m
    rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]
    · simp only [↓reduceIte, one_smul]
    simp only [orthonormal_iff_ite.1 w.orthonormal, ite_smul, one_smul, zero_smul,
      ite_eq_right_iff]
    tauto
  _ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪v i, w n⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by
    simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
  _ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪w n, v i⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by
    simp only [real_inner_comm (w _)]
  _ = ∑ i, (∑ m, ⟪w m, v i⟫_ℝ • w m) ⊗ₜ[ℝ] ∑ n, ⟪w n, v i⟫_ℝ • w n := by
    simp only [sum_tmul, tmul_sum, smul_tmul_smul, Finset.sum_comm (γ := ι), Finset.sum_smul]
    rw [Finset.sum_comm]
  _ = ∑ i, v i ⊗ₜ[ℝ] v i := by
    simp only [w.sum_repr' (v _)]

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

Goal state before:
pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
rw [div_mul_comm, div_self (by norm_cast; linarith)]

Goal state after:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
rw [div_mul_comm, div_self (by norm_cast; linarith)]

Goal state after:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + ((↑u - ↑l) / (↑u - ↑l) * z - ↑l / (↑u - ↑l) * (↑u - ↑l)) = z

Tactic:
div_self (by norm_cast; linarith),

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (1 * z - ↑l / (↑u - ↑l) * (↑u - ↑l)) = z
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ z.re * ((u - l) / (u - l) / (u - l)) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)

Tactic:
div_self (by norm_cast; linarith),

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re * (1 / (u - l)) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
⊢ ContDiffWithinAt ℝ 2 f₂ s y → y ∈ insert x s → (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y

Tactic:
h₂y

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
⊢ y ∈ insert x s → (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
⊢ ContDiffWithinAt ℝ 2 f₂ s y → y ∈ insert x s → (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y

Tactic:
h₂y

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
⊢ y ∈ insert x s → (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ DifferentiableAt ℂ (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) x

Tactic:
have : (fun z ↦ fderiv ℝ f z 1 - I * fderiv ℝ f z I) =
      (ofRealCLM ∘ (fderiv ℝ f · 1) - I • ofRealCLM ∘ (fderiv ℝ f · I)) := by
    ext; simp
  rw [this]
  have h₁f := hf.1
  refine differentiableAt_complex_iff_differentiableAt_real.2 ⟨by fun_prop, ?_⟩
  rw [fderiv_sub (by fun_prop) (by fun_prop), fderiv_const_smul (by fun_prop)]
  repeat rw [fderiv_comp]; all_goals try fun_prop
  simp only [ContinuousLinearMap.fderiv, sub_apply, ContinuousLinearMap.comp_apply, ofRealCLM_apply,
    smul_apply, smul_eq_mul]
  ring_nf
  rw [fderiv_clm_apply (by fun_prop) (by fun_prop), fderiv_clm_apply (by fun_prop) (by fun_prop)]
  simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,
    ContinuousLinearMap.flip_apply, I_sq, neg_mul, one_mul, sub_neg_eq_add]
  rw [add_comm, sub_eq_add_neg]
  congr 1
  · norm_cast
    apply h₁f.isSymmSndFDerivAt (by simp)
  · have h₂f := hf.2.eq_of_nhds
    simp only [laplacian_eq_iteratedFDeriv_complexPlane, iteratedFDeriv_two_apply, Fin.isValue,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Pi.zero_apply,
      add_eq_zero_iff_eq_neg] at h₂f
    simp [h₂f]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
⊢ μ s = μ (Ι a b)

Tactic:
measure_congr hs_ev

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
⊢ μ (Ι a b) = μ (Ι a b)