mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case hsm
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := ⋯
B : s = ⋃ n, t n
⊢ ∀ (i : ℕ), MeasurableSet (t i)

Tactic:
intro n

Goal state after:
case hsm
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := fun n ↦ closure[inst✝⁴] (compactCovering β n) ∩ s
B : s = ⋃ n, t n
n : ℕ
⊢ MeasurableSet (t n)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hh
a b : ℝ
⊢ Tendsto (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)

Tactic:
apply tendsto_volume_totalLengthFilter_nhds_zero.mono_left

Goal state after:
case hh
a b : ℝ
⊢ totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤ totalLengthFilter
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case hf
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := ⋯
s : Set ℝ := ⋯
x : ℝ
hx : x ∈ s
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ∃ a ∈ t, (Prod.snd - Prod.fst) a = x_1 ∧ a.1 = x

Tactic:
have := hasDerivAt_iff_tendsto_slope.mp hx.right

Goal state after:
case hf
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ∃ a ∈ t, (Prod.snd - Prod.fst) a = x_1 ∧ a.1 = x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ dist (f d) (f b) ≤ y

Tactic:
replace hu₂ (s : Finset u) : (SetLike.coe (u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2 :=
    hu₂.subset (by grind)

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
⊢ dist (f d) (f b) ≤ y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
⊢ MapsTo T univ (disjWithin d b)

Tactic:
intro s _

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
s : Finset ↑u
a✝ : s ∈ univ
⊢ T s ∈ disjWithin d b
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / - -((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
neg_neg

Goal state after:
case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case right
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
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
ε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)
p :
  ∀ ε > 0,
    ∃ N,
      ∀ n ≥ N, dist ((1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) (l - ∑' (n : ℕ), f n * z ^ n) < ε
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

Tactic:
dist_eq_norm,

Goal state after:
case right
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
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
ε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)
p :
  ∀ ε > 0,
    ∃ N, ∀ n ≥ N, ‖(1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i - (l - ∑' (n : ℕ), f n * z ^ n)‖ < ε
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
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
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖

Tactic:
have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel

Goal state after:
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
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
⊢ ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: x : ℝ
⊢ deriv^[2] (fun x ↦ √x * log x) x = -log x / (4 * √x ^ 3)

Tactic:
simp only [Nat.iterate, deriv_sqrt_mul_log']
  rcases le_or_gt x 0 with hx | hx
  · rw [sqrt_eq_zero_of_nonpos hx, zero_pow three_ne_zero, mul_zero, div_zero]
    refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)
    refine (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => ?_) hx
    rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
  · have h₀ : √x ≠ 0 := sqrt_ne_zero'.2 hx
    convert!
      (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
          mul_ne_zero two_ne_zero h₀).deriv using 1
    nth_rw 3 [← mul_self_sqrt hx.le]
    field

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

Goal state before:
pp: θ : ℂ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Tactic:
exact cos_eq_zero_iff

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

Goal state before:
pp: 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 ∈ Ioo x w, deriv f a < (f w - f x) / (w - x)

Tactic:
apply StrictMonoOn.exists_deriv_lt_slope_aux _ hxw _ _
      · exact hf.mono (Icc_subset_Icc le_rfl hwy.le)
      · exact hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)
      · intro z hz
        rw [← hw]
        apply ne_of_lt
        exact hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2

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

Goal state before:
pp: z w : ℂ
⊢ cos z - w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
simpa [field, cos, exp_neg] using Eq.congr (by ring) rfl

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

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ ∀ x ∈ interior (interior D), 0 ≤ deriv (deriv f) x

Tactic:
by
        rwa [interior_interior]

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

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x ≤ 0

Tactic:
by
        rwa [interior_interior]

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

Goal state before:
pp: case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r * 2 ≤ -1 - 1

Tactic:
← le_div_iff₀

Goal state after:
case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ (-1 - 1) / 2

case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 0 < 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

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:
sqrt_one

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.Arctan

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ arctan x = arccos (√(1 + x ^ 2))⁻¹

Tactic:
arctan_eq_arcsin,

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arccos (√(1 + x ^ 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x < 0
this : arctan x⁻¹ = -(π / 2) - - -arctan x
⊢ arctan x⁻¹ = -(π / 2) - arctan x

Tactic:
neg_neg

Goal state after:
x : ℝ
h : x < 0
this : arctan x⁻¹ = -(π / 2) - arctan x
⊢ arctan x⁻¹ = -(π / 2) - arctan x
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x✝ y x : ℂ
hx : ‖x‖ = 1
hy : ‖1‖ = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)

Tactic:
norm_eq_one_iff'

Goal state after:
x✝ y x : ℂ
hx : ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x
hy : ‖1‖ = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
Module: Mathlib.Analysis.Normed.Module.Ball.Action

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(closedBall 0 r)
⊢ ‖↑c • ↑x‖ ≤ r

Tactic:
by
        simpa only [norm_smul, one_mul] using
          mul_le_mul (mem_closedBall_zero_iff.1 c.2) (mem_closedBall_zero_iff.1 x.2) (norm_nonneg _)
            zero_le_one

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
⊢ f =ᶠ[𝓝[≠] x] 0

Tactic:
rw [← hf.frequently_zero_iff_eventuallyEq_zero]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
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 : AnalyticAt 𝕜 f x
h₂f : analyticOrderAt f x = ⊤
⊢ MeromorphicNFAt f x

Tactic:
analyticOrderAt_eq_top

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
⊢ MeromorphicNFAt f x
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
a₁ : ℤ
ha₁ : ↑a₁ = meromorphicOrderAt f₁ z
a₂ : ℤ
ha₂ : ↑a₂ = meromorphicOrderAt f₂ z
⊢ (divisor (f₁ • f₂) U) z = (divisor f₁ U + divisor f₂ U) z

Tactic:
simp [h₁f₁, h₁f₂, h₁f₁.smul h₁f₂, hz, meromorphicOrderAt_smul (h₁f₁ z hz) (h₁f₂ z hz),
      ← ha₁, ← ha₂, ← WithTop.coe_add]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
this : ∀ {μ : ι}, μ ∈ s.erase τ → f μ x ≠ 0
⊢ MeromorphicNFAt (f τ * ∏ x ∈ s.erase τ, f x) x

Tactic:
meromorphicNFAt_mul_iff_left

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
this : ∀ {μ : ι}, μ ∈ s.erase τ → f μ x ≠ 0
⊢ MeromorphicNFAt (f τ) x

case neg.h₁g
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
this : ∀ {μ : ι}, μ ∈ s.erase τ → f μ x ≠ 0
⊢ AnalyticAt 𝕜 (∏ x ∈ s.erase τ, f x) x

case neg.h₂g
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
this : ∀ {μ : ι}, μ ∈ s.erase τ → f μ x ≠ 0
⊢ (∏ x ∈ s.erase τ, f x) x ≠ 0
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
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hord : analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicNFAt (f ∘ g) x

Tactic:
analyticOrderAt_eq_top

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hord : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = 0
⊢ MeromorphicNFAt (f ∘ g) x
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 : 𝕜
hf : MeromorphicAt f x
h : analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0

Tactic:
analyticOrderAt_eq_top

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0
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 : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤

Tactic:
analyticOrderAt_eq_top

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
m : ℕ
hm : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
h₂ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x

Tactic:
· simp_all [meromorphicOrderAt_congr h]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
h₂ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
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 : analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
⊢ ¬∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
analyticOrderAt_eq_top

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
⊢ ¬∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg.h₁g
𝕜 : 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 = ⊤
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
⊢ AnalyticAt 𝕜 (-g) x

pp: case neg.h
𝕜 : 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 = ⊤
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
⊢ -f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) z

Tactic:
· fun_prop

Goal state after:
case neg.h
𝕜 : 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 = ⊤
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
⊢ -f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) z