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

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

Tactic:
simp only [div_lt_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ M ≠ 0

Tactic:
by linarith only [hM]

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

Goal state before:
pp: x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ cos (x / 2) ^ 2 - sin (x / 2) ^ 2 = (1 - tan (x / 2) ^ 2) * cos (x / 2) ^ 2

Tactic:
← tan_mul_cos this

Goal state after:
x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ cos (x / 2) ^ 2 - (tan (x / 2) * cos (x / 2)) ^ 2 = (1 - tan (x / 2) ^ 2) * cos (x / 2) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 < x ^ 2

Tactic:
wlog! hx₀ : 0 < x
  case inr =>
    simpa using this (neg_ne_zero.2 hx) <| neg_pos_of_neg <| hx.lt_of_le hx₀
  rcases le_or_gt x 1 with hxπ | hxπ
  case inl =>
    exact pow_lt_pow_left₀ (sin_lt hx₀)
      (sin_nonneg_of_nonneg_of_le_pi hx₀.le (by linarith [two_le_pi])) (by simp)
  case inr =>
    exact (sin_sq_le_one _).trans_lt (by rwa [one_lt_sq_iff₀ hx₀.le])

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

Goal state before:
pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √(1 - x ^ 2 + x ^ 2))

pp: case hb
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

pp: case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
sub_add_cancel

Goal state after:
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √1)

case hb
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inr
x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 ≤ cos x

Tactic:
case inr => exact (one_sub_sq_div_two_lt_cos hx).le

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

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x = arctan (√(1 - x ^ 2) / x)

Tactic:
eq_comm

Goal state after:
x : ℝ
h : 0 < x
⊢ arctan (√(1 - x ^ 2) / x) = π / 2 - arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y ^ 2 + 1 < 1 + tan y ^ 2

Tactic:
add_comm,

Goal state after:
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ 1 + y ^ 2 < 1 + tan y ^ 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)

Tactic:
refine hfc.secant_mono hy hx (?_ : t ∈ S) hxy.ne ht'.ne ht.le

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ t ∈ S
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
← real_inner_div_norm_mul_norm_eq_one_iff,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = 0 ↔ ⟪x, y⟫ / (‖x‖ * ‖y‖) = 1
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ 1 = ⟪x, y⟫ / (‖x‖ * ‖y‖) ↔ ⟪x, y⟫ / (‖x‖ * ‖y‖) = 1

pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) ≤ 1

Tactic:
eq_comm

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) = 1 ↔ ⟪x, y⟫ / (‖x‖ * ‖y‖) = 1

V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) ≤ 1
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_2
z x✝ : ℂ
⊢ (∃ n, x✝ = z + ↑n * (2 * ↑Real.pi * I)) ↔ x✝ + -z ∈ AddSubgroup.zmultiples (2 * ↑Real.pi * I)

Tactic:
AddSubgroup.mem_zmultiples_iff,

Goal state after:
case refine_2
z x✝ : ℂ
⊢ (∃ n, x✝ = z + ↑n * (2 * ↑Real.pi * I)) ↔ ∃ k, k • (2 * ↑Real.pi * I) = x✝ + -z
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_2
z x✝ : ℂ
⊢ (∃ n, x✝ = z + ↑n * (2 * ↑Real.pi * I)) ↔ ∃ k, x✝ = k • (2 * ↑Real.pi * I) + z

Tactic:
add_comm,

Goal state after:
case refine_2
z x✝ : ℂ
⊢ (∃ n, x✝ = z + ↑n * (2 * ↑Real.pi * I)) ↔ ∃ k, x✝ = z + k • (2 * ↑Real.pi * I)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
rw [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← dist_eq_norm_sub,
      ← dist_eq_norm_sub, ← div_eq_inv_mul, div_le_iff₀]

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ 0 < dist z c
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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
h₁z : z = x
⊢ f z = ((fun x_1 ↦ x_1 - x) ^ n • g) z

Tactic:
simp only [h₁z, Pi.smul_apply', Pi.pow_apply, sub_self]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
h₁z : z = x
⊢ f x = 0 ^ n • g x
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
⊢ (divisor (fun x ↦ x - z₀) U) x = 0

Tactic:
by
  by_cases hu : x ∈ U
  · rw [divisor_apply (show MeromorphicOn (· - z₀) U from fun_sub id <| const z₀) hu,
      ← untop₀_coe 0]
    congr
    exact (meromorphicOrderAt_eq_int_iff (by fun_prop)).mpr
      ⟨(· - z₀), analyticAt_id.fun_sub analyticAt_const, by simp [sub_ne_zero_of_ne hx]⟩
  · exact Function.locallyFinsuppWithin.apply_eq_zero_of_notMem _ hu

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
y : 𝕜
hy : y ∈ (g ⁻¹' {0})ᶜ
⊢ f y = (g⁻¹ • g • f) y

Tactic:
Set.mem_compl_iff,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
y : 𝕜
hy : y ∉ g ⁻¹' {0}
⊢ f y = (g⁻¹ • g • f) y
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case right
𝕜 : 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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ toMeromorphicNFAt f x x = (x - x) ^ n • g x

Tactic:
simp only [toMeromorphicNFAt, hf, ↓reduceDIte, ← hn, WithTop.coe_zero,
        WithTop.coe_eq_zero, ne_eq, Function.update_self, sub_self]

Goal state after:
case right
𝕜 : 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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ (if h : n = 0 then Classical.choose ⋯ x else 0) = 0 ^ n • g x
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
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
hf : MeromorphicAt f x
⊢ toMeromorphicNFAt f x =ᶠ[𝓝 x] toMeromorphicNFAt g x

Tactic:
exact meromorphicNFAt_toMeromorphicNFAt.eventuallyEq_nhdsNE_iff_eventuallyEq_nhds
        meromorphicNFAt_toMeromorphicNFAt |>.mp <| hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans
      <| hfg.trans ((MeromorphicAt.meromorphicAt_congr hfg).mp hf).eq_nhdsNE_toMeromorphicNFAt

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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt (f₁ + f₂) x

Tactic:
add_comm,

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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt (f₂ + f₁) x
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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    ((fun x_1 ↦ x_1 - x) ^ n • g) x

Tactic:
eq_comm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
⊢ ((fun x_1 ↦ x_1 - x) ^ n • g) x =
    (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      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
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
τ₀ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + (z - x) ^ (n₂ - n₁) • g₂) z
τ₁ : AnalyticAt 𝕜 (fun z ↦ g₁ z + (z - x) ^ (n₂ - n₁) • g₂ z) x
τ₂ : g₁ x + (x - x) ^ (n₂ - n₁) • g₂ x ≠ 0
⊢ 0 ^ (n₂ - n₁) = 0 ∨ g₂ x = 0

Tactic:
zero_zpow _ (sub_ne_zero.2 (ne_of_lt h).symm)

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
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
τ₀ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + (z - x) ^ (n₂ - n₁) • g₂) z
τ₁ : AnalyticAt 𝕜 (fun z ↦ g₁ z + (z - x) ^ (n₂ - n₁) • g₂ z) x
τ₂ : g₁ x + (x - x) ^ (n₂ - n₁) • g₂ x ≠ 0
⊢ 0 = 0 ∨ g₂ x = 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

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

Tactic:
ext z
  by_cases hz : z ∈ U <;> simp [hf, (meromorphicNFOn_toMeromorphicNFOn f U).meromorphicOn, hz]

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
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

Tactic:
by
  by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤
  · simp_all [meromorphicOrderAt_smul hf₁ hf₂]
  by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
  · simp_all [meromorphicOrderAt_smul hf₁ hf₂]
  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_ne_top_iff hf₁).1 h₁f₁
  obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_ne_top_iff hf₂).1 h₁f₂
  have : f₁ • f₂ =ᶠ[𝓝[≠] x]
      fun z ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z := by
    filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin] with y h₁y h₂y h₃y
    simp_all [meromorphicOrderAt_smul hf₁ hf₂, zpow_add₀ (sub_ne_zero.2 h₃y)]
    module
  rw [h₁g₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g₁ h₃g₁,
    h₁g₂.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g₂ h₃g₂,
    (h₁g₁.smul h₁g₂).meromorphicTrailingCoeffAt_of_eq_nhdsNE this]
  simp

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

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

Tactic:
simp [hf₁, this]

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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
eq_comm

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₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
⊢ meromorphicOrderAt f₂ x = meromorphicOrderAt f₁ x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case pos
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
ta : ↑I × A
_ : ¬ta.1 ≤ t n
hv : f ta ∈ (q e).target
⊢ p (↑(q e).symm (f ta)) = f ta

Tactic:
rw [hpq e, (q e).right_inv hv]

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₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
by
  by_cases hf₁ : MeromorphicAt f₁ x; swap
  · have : ¬ MeromorphicAt f₂ x := by
      contrapose hf₁
      exact hf₁.congr hf₁₂.symm
    simp [hf₁, this]
  rw [eq_comm]
  cases h₁f₁ : meromorphicOrderAt f₁ x with
  | top =>
    rw [meromorphicOrderAt_eq_top_iff] at h₁f₁ ⊢
    filter_upwards [hf₁₂, h₁f₁] using by grind
  | coe n =>
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 h₁f₁
    rw [meromorphicOrderAt_eq_int_iff (hf₁.congr hf₁₂)]
    use g, h₁g, h₂g
    filter_upwards [hf₁₂, h₃g] using by grind

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
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ ⊤ = meromorphicOrderAt (-f) x

Tactic:
eq_comm

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (-f) x = ⊤
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 : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
⊢ ↑n * meromorphicOrderAt f x + meromorphicOrderAt f x = (↑n + 1) * meromorphicOrderAt f x

Tactic:
cases meromorphicOrderAt f x

Goal state after:
case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
⊢ ↑n * ⊤ + ⊤ = (↑n + 1) * ⊤

case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * ↑a✝ + ↑a✝ = (↑n + 1) * ↑a✝
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₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
add_comm,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₂ + f₁) x = meromorphicOrderAt 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
x : 𝕜
hx : D x ≠ 0
⊢ ¬z = x

Tactic:
eq_comm

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
x : 𝕜
hx : D x ≠ 0
⊢ ¬x = z
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
⊢ g ∈ (scalar n).range → g ∈ Subgroup.center (GL n R)

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
a : Rˣ
⊢ (scalar n) a ∈ Subgroup.center (GL n R)
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
hsq : normSq (f z) + normSq 1 - 2 * (f z * (starRingEnd ℂ) 1).re = normSq z + normSq 1 - 2 * (z * (starRingEnd ℂ) 1).re
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
simpa [normSq_eq_norm_sq, Complex.add_conj, LinearIsometry.norm_map] using hsq.symm

Goal state after: