mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
⊢ HasDerivWithinAt (fun t ↦ ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y

Tactic:
rw [this]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
⊢ HasDerivWithinAt (fun t ↦ ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)) t
    y
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ Icc a a
hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !

Tactic:
rw [Icc_self, mem_singleton_iff] at hx
    simp [hx]

Goal state after:
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
H : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : E
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
this : f = (⇑A.symm ∘ ⇑A) ∘ f
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
rw [this]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
H : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : E
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
this : f = (⇑A.symm ∘ ⇑A) ∘ f
⊢ DifferentiableWithinAt ℝ ((⇑A.symm ∘ ⇑A) ∘ f) s x
Module: Mathlib.Analysis.Calculus.TaylorIntegral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
t : ℝ
this : -((↑n !)⁻¹ * (1 - t) ^ n) = (↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)
⊢ HasDerivAt (fun t ↦ (↑(n + 1)!)⁻¹ * (1 - t) ^ (n + 1)) (-((↑n !)⁻¹ * (1 - t) ^ n)) t

Tactic:
rw [this]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
t : ℝ
this : -((↑n !)⁻¹ * (1 - t) ^ n) = (↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)
⊢ HasDerivAt (fun t ↦ (↑(n + 1)!)⁻¹ * (1 - t) ^ (n + 1)) ((↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)) t
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case a
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ ↑p.2 p.1 - ↑p.2 0 < δ

Tactic:
linarith [mem_Icc.mp (hp₂ p.1), mem_Icc.mp (hp₂ 0)]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ (∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i))).toReal =
    ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))

Tactic:
ENNReal.toReal_sum (by simp [edist_ne_top])

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ ∑ a ∈ Finset.range p.1, (edist (f (↑p.2 (a + 1))) (f (↑p.2 a))).toReal =
    ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ M, 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
use M

Goal state after:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x

Tactic:
rw [← AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub hf hg,
      ← intervalIntegral.integral_sub]

Goal state after:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ ∫ (x : ℝ) in a..b, f x * deriv g x = ∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x - deriv f x * g x

case hf
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (fun x ↦ deriv f x * g x + f x * deriv g x) volume a b

case hg
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (fun x ↦ deriv f x * g x) volume a b
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ε - (ε / 3 + ε / 3) ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖)

Tactic:
gcongr
        · exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _
        · exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ √x * log x) x = 0

Tactic:
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x ↦ √x * log x) 0 (Iic 0) x
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ (2 + log x) / (2 * √x)) x = 0

Tactic:
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Goal state after:
case inl
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x ↦ (2 + log x) / (2 * √x)) 0 (Iic 0) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x y : ℂ
⊢ cos x - cos y = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0

Tactic:
cos_sub_cos

Goal state after:
x y : ℂ
⊢ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
⊢ ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z

Tactic:
filter_upwards [hf, h1] with z h using h.inv

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

Goal state before:
pp: x : ℂ
h : cos x = 0
k : ℤ
hxk : x = (2 * ↑k + 1) * ↑π / 2
⊢ ↑(2 * k + 1) * ↑π / 2 = x

Tactic:
by simp [hxk]

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

Goal state before:
pp: x : ℂ
⊢ tan x = 2 * tan (x / 2) / (1 - tan (x / 2) ^ 2)

Tactic:
by
  conv_lhs => rw [← mul_div_cancel₀ x two_ne_zero, tan_two_mul]

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

Goal state before:
pp: case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ -2 * sin (a / 2) * sin (a * ↑x + b) = cos (a * (↑(x + 1) - 1 / 2) + b) - cos (-(a * (↑x - 1 / 2) + b))

Tactic:
cos_sub_cos

Goal state after:
case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ -2 * sin (a / 2) * sin (a * ↑x + b) =
    -2 * sin ((a * (↑(x + 1) - 1 / 2) + b + -(a * (↑x - 1 / 2) + b)) / 2) *
      sin ((a * (↑(x + 1) - 1 / 2) + b - -(a * (↑x - 1 / 2) + b)) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ cos (a * (↑n - 1 / 2) + b) - cos (a * (↑0 - 1 / 2) + b) = -2 * sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b)

Tactic:
cos_sub_cos

Goal state after:
n : ℕ
a b : ℂ
⊢ -2 * sin ((a * (↑n - 1 / 2) + b + (a * (↑0 - 1 / 2) + b)) / 2) *
      sin ((a * (↑n - 1 / 2) + b - (a * (↑0 - 1 / 2) + b)) / 2) =
    -2 * sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ sin (arctan x) ^ 2 = x ^ 2 / (1 + x ^ 2)

Tactic:
rw [← tan_sq_div_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]

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

Goal state before:
pp: x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 1 + 2 / π * x ≤ cos x

Tactic:
by
  simpa using one_sub_mul_le_cos (x := -x) (by linarith) (by linarith)

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

Goal state before:
pp: x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))

Tactic:
exact tan_add' ⟨arctan_ne_mul_pi_div_two, arctan_ne_mul_pi_div_two⟩

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ sin (arctan x) ↔ 0 ≤ x

Tactic:
by
  simpa using sin_arctan_strictMono.le_iff_le (a := 0)

Goal state after:
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:
by
  simp [← cos_angle_mul_norm_mul_norm, h]

Goal state after:
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 = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖

Tactic:
by
  simp [← cos_angle_mul_norm_mul_norm, h]

Goal state after:
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ Tendsto (fun n ↦ z ^ n) atTop (𝓝 0)

Tactic:
simp only [isEmbedding_coe.tendsto_nhds_iff, comp_def, coe_pow]
  exact tendsto_pow_atTop_nhds_zero_iff_norm_lt_one.mpr z.norm_lt_one
    |>.comp tendsto_PNat_val_atTop_atTop

Goal state after:
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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬meromorphicOrderAt g x = 0
⊢ f x = g x

Tactic:
hg.meromorphicOrderAt_eq_zero_iff

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬g x ≠ 0
⊢ f x = g x
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
⊢ (divisor (f ∘ fun x ↦ x - c) U) (z + c) = (divisor f (U - {c})) z

Tactic:
rw [sub_eq_add_neg, Set.neg_singleton, ← divisor_comp_add_const_eq_divisor]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
⊢ (divisor (f ∘ fun x ↦ x - c) U) (z + c) = (divisor (f ∘ fun x ↦ x + -c) U) (z - -c)
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
⊢ MeromorphicNFAt (f / g) x

Tactic:
rw [div_eq_mul_inv]
  rcases hor with hgne | hfne
  · have hf := hf.meromorphicNFAt
    have hgAnalytic : AnalyticAt 𝕜 g x := by grind [meromorphicNFAt_iff_analyticAt_or]
    have hgInvAnalytic : AnalyticAt 𝕜 g⁻¹ x := hgAnalytic.inv hgne
    rwa [← meromorphicNFAt_mul_iff_left hgInvAnalytic (inv_ne_zero hgne)] at hf
  · grind [meromorphicNFAt_mul_iff_right, hg.inv]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicNFAt f (x + c)
⊢ MeromorphicNFAt (f ∘ fun x ↦ x + c) x

Tactic:
· exact h.comp_analyticAt (g := fun z ↦ z + c) (by fun_prop)

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
x : 𝕜
hf : MeromorphicAt f x
x✝¹ : 𝕜
x✝ : x✝¹ ∈ {x}ᶜ
⊢ f x✝¹ = toMeromorphicNFAt f x x✝¹

Tactic:
by simp_all [toMeromorphicNFAt]

Goal state after:
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
      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf).1 hn.symm
      right
      use n, g, h₁g, h₂g
      apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE (hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans h₃g)
      simp only [toMeromorphicNFAt, hf, ↓reduceDIte, ← hn, WithTop.coe_zero,
        WithTop.coe_eq_zero, ne_eq, Function.update_self, sub_self]
      split_ifs with h₃f
      · obtain ⟨h₁G, _, h₃G⟩ :=
          Classical.choose_spec ((meromorphicOrderAt_eq_int_iff hf).1 (h₃f ▸ hn.symm))
        apply Filter.EventuallyEq.eq_of_nhds
        apply (h₁G.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop)).1
        filter_upwards [h₃g, h₃G]
        simp_all
      · simp [h₃f, zero_zpow]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicNFOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : ∃ x ∈ U, x + c = y
⊢ MeromorphicNFAt f y

Tactic:
obtain ⟨x, h₁x, h₂x⟩ := hy

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicNFOn (f ∘ fun x ↦ x + c) U
y x : 𝕜
h₁x : x ∈ U
h₂x : x + c = y
⊢ MeromorphicNFAt f y
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
this : 0 = (x - x) ^ n • g x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
rw [this]

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) (𝓝 ((x - x) ^ n • g x))
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hn : analyticOrderAt f x = ⊤
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ⊤

pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
a✝ : ℕ
hn : analyticOrderAt f x = ↑a✝
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ↑a✝

Tactic:
· rw [ENat.map_top, meromorphicOrderAt_eq_top_iff]
    exact (analyticOrderAt_eq_top.mp hn).filter_mono nhdsWithin_le_nhds

Goal state after:
case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
a✝ : ℕ
hn : analyticOrderAt f x = ↑a✝
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ↑a✝
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ meromorphicOrderAt ((fun x_1 ↦ x_1 - x) ^ n) x = ↑n

Tactic:
meromorphicOrderAt_eq_int_iff (by fun_prop)

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, ((fun x_1 ↦ x_1 - x) ^ n) z = (z - x) ^ n • g z
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
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
hn : meromorphicOrderAt f x = ↑n
⊢ meromorphicOrderAt (-f) x = ↑n

Tactic:
meromorphicOrderAt_eq_int_iff (by fun_prop)

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
hn : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
a : ℤ
ha : ↑a = meromorphicOrderAt f x
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ a • g x_1
a✝ : 𝕜
h₁a : a✝ ∈ {x}ᶜ → f a✝ = (a✝ - x) ^ a • g a✝
h₂a : a✝ ∈ {x}ᶜ
⊢ f⁻¹ a✝ = (a✝ - x) ^ (-a) • g⁻¹ a✝

Tactic:
simp [h₁a h₂a, Algebra.smul_def, mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case refine_1
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ r * ↑g⁻¹ i i = 1

Tactic:
simpa [-mul_inv_cancel, ← hr, ← pow_succ',
      Nat.sub_one_add_one Fintype.card_pos.ne.symm] using
        Matrix.ext_iff.2 (Subtype.ext_iff.1 (mul_inv_cancel g)) i i

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
⊢ ℓ ((↑a.re + ↑a.im * I) • b) = (↑a.re + ↑a.im * I) • ℓ b

Tactic:
← re_add_im b,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
⊢ ℓ ((↑a.re + ↑a.im * I) • (↑b.re + ↑b.im * I)) = (↑a.re + ↑a.im * I) • ℓ (↑b.re + ↑b.im * I)