mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case inr
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset ↑u), ∑ z ∈ s, g z ≤ r
hu₄ : HasSum g (∑' (b : ↑u), g b)
g_sum_bound : ∑' (x : ↑u), g x ≤ r
⊢ dist (f d) (f b) ≤ r

Tactic:
have := (hf.mono (by grind [uIcc_of_le])).dist_le_of_pairwiseDisjoint_hasSum hd.right
    (fun s hs ↦ hu₁ s hs |>.left) hu₂ hu₃ hu₄

Goal state after:
case inr
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset ↑u), ∑ z ∈ s, g z ≤ r
hu₄ : HasSum g (∑' (b : ↑u), g b)
g_sum_bound : ∑' (x : ↑u), g x ≤ r
this : dist (f d) (f b) ≤ ∑' (b : ↑u), g b
⊢ dist (f d) (f b) ≤ r
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

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

Tactic:
by
  have f_deriv_integral_ac :=
    hf.intervalIntegrable_deriv.absolutelyContinuousOnInterval_intervalIntegral
    (c := a) (by simp)
  let g (x : ℝ) := f x - ∫ (t : ℝ) in a..x, deriv f t
  have g_ac : AbsolutelyContinuousOnInterval g a b := hf.sub (f_deriv_integral_ac)
  have g_ae_deriv_zero : ∀ᵐ x, x ∈ uIcc a b → HasDerivAt g 0 x := by
    filter_upwards [hf.ae_differentiableAt, hf.intervalIntegrable_deriv.ae_hasDerivAt_integral]
      with x hx₁ hx₂ hx₃
    convert! (hx₁ hx₃).hasDerivAt.sub (hx₂ hx₃ a (by simp))
    abel
  obtain ⟨C, hC⟩ := g_ac.const_of_ae_hasDerivAt_zero g_ae_deriv_zero
  have : f a = g a := by simp [g]
  have := hC a (by simp)
  have := hC b (by simp)
  grind

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall 0 r
hy : y ∈ closedBall 0 r
⊢ a • x + b • y ∈ ball 0 r

Tactic:
exact combo_mem_ball_of_ne hx hy hne ha hb hab

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hx : ‖x‖ ≤ r
hy : ‖y‖ ≤ r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ‖a • x + b • y‖ < r

Tactic:
by
  simp only [← mem_ball_zero_iff, ← mem_closedBall_zero_iff] at hx hy ⊢
  exact combo_mem_ball_of_ne hx hy hne ha hb hab

Goal state after:
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 - δ'
z : E
hz : 1 - δ' < ‖z‖
⊢ ‖z‖⁻¹ * ‖z‖ = 1

Tactic:
inv_mul_cancel₀ (hδ'.trans hz).ne'

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 - δ'
z : E
hz : 1 - δ' < ‖z‖
⊢ 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ (∃ n, ↑n * (2 * π) = x) ∨ cos x = -1 ↔ ∃ k, ↑k * π = x

Tactic:
cos_eq_neg_one_iff

Goal state after:
x : ℝ
⊢ ((∃ n, ↑n * (2 * π) = x) ∨ ∃ k, π + ↑k * (2 * π) = x) ↔ ∃ k, ↑k * π = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

Tactic:
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_left₀ (half_pos pi_pos)]

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

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

Tactic:
rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul,
    mul_div_cancel₀, sub_add_cancel, sqrt_one, div_one] <;> simp at h

Goal state after:
case hb
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0

case hx
x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2

x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0

x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: y : ℂ
hy : y ≠ 0
⊢ angle 1 y = |y.arg|

Tactic:
by simp [angle_eq_abs_arg, hy]

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

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

Tactic:
wlog h : y = 1

Goal state after:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

x✝ y✝ x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
Module: Mathlib.Analysis.Meromorphic.Divisor

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

Tactic:
by_cases h₂ : meromorphicOrderAt f₂ z = ⊤

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

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
⊢ divisor (f ^ n) U = n • divisor f U

Tactic:
ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]
  · simp [hz]

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

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

Tactic:
· 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
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
⊢ toMeromorphicNFAt f x =ᶠ[𝓝 x] toMeromorphicNFAt g x

Tactic:
by
  by_cases hf : MeromorphicAt f x
  · 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
  · simp [hf, MeromorphicAt.meromorphicAt_congr hfg |>.not.mp]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support.Finite
⊢ MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) U = D

Tactic:
by
  ext z
  by_cases hz : z ∈ U
  <;> simp [(meromorphicNFOn D U).meromorphicOn, hz, meromorphicOrderAt_eq D hD]

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

Goal state before:
pp: R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖↑R ^ 2 - (starRingEnd ℂ) w * z‖ / ‖↑R * (z - w)‖ = 1

Tactic:
div_eq_iff (by rw [ne_eq, norm_eq_zero]; positivity),

Goal state after:
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖↑R ^ 2 - (starRingEnd ℂ) w * z‖ = 1 * ‖↑R * (z - w)‖
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 : 𝕜 → 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
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt φ⁻¹ z ≠ ⊤

Tactic:
simpa [meromorphicOrderAt_inv] using meromorphicOrderAt_ne_top (divisor f U)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
z : ℂ
hR : 0 < R
⊢ meromorphicOrderAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z ≠ ⊤

Tactic:
apply meromorphicOrderAt_finprod_ne_top
    (fun _ ↦ MeromorphicAt.zpow (meromorphic_canonicalFactor _ _ _) _)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
z : ℂ
hR : 0 < R
⊢ ∀ (c : ℂ), meromorphicOrderAt (canonicalFactor R c ^ (divisor f (ball 0 R)) c) z ≠ ⊤
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
⊢ ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t (n + 1))) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t (n + 1))) ∧ Γ 0 = e

Tactic:
have pΓtn : p (Γ (t n)) = γ (t n) := eqOn ⟨t_0 ▸ t_mono n.zero_le, le_rfl⟩

Goal state after:
case succ
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
⊢ ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t (n + 1))) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t (n + 1))) ∧ Γ 0 = e
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
⊢ AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x

Tactic:
refine analyticAt_finprod fun a ↦ ?_

Goal state after:
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 : ℂ
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
have : meromorphicOrderAt (∏ᶠ u, canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x = 0 := by
      refine η₁.meromorphicNFAt.meromorphicOrderAt_eq_zero_iff.2 (finprod_apply_ne_zero fun a ↦ ?_)
      by_cases ha : a ∈ ball 0 R
      · exact zpow_ne_zero _ (canonicalFactor_ne_zero ha (by aesop) (by aesop))
      · simp_all

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
this : meromorphicOrderAt (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x = 0
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ rexp 1 + 1 / 2 < ↑3 + 1

Tactic:
grind [exp_one_lt_three]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
e_1✝ : ↑(p ⁻¹' {{ toFun := p, continuous_toFun := ⋯ } ↑ey}) = ↑(p ⁻¹' {y})
e_7✝ : { toFun := p, continuous_toFun := ⋯ } ↑ex = x
e_8✝ : { toFun := p, continuous_toFun := ⋯ } ↑ey = y
⊢ Γ.map { toFun := p, continuous_toFun := ⋯ } ≍ γ

Tactic:
eq

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
e_1✝ : ↑(p ⁻¹' {{ toFun := p, continuous_toFun := ⋯ } ↑ey}) = ↑(p ⁻¹' {y})
e_7✝ : { toFun := p, continuous_toFun := ⋯ } ↑ex = x
e_8✝ : { toFun := p, continuous_toFun := ⋯ } ↑ey = y
⊢ γ.cast ⋯ ⋯ ≍ γ
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
hz : deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z
hzx : z - x ≠ 0
⊢ (z - x) ^ n • deriv g z + (↑n * (z - x) ^ (n - 1)) • g z = (z - x) ^ (n - 1) • (↑n • g z + (z - x) • deriv g z)

Tactic:
by
      simp [smul_smul, ← zpow_add_one₀ hzx, add_comm, mul_comm]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x y : X
γ γ' : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
eq : ⋯.monodromy γ e = ⋯.monodromy γ' e
g : G
⊢ ↑(((hp.toPermFiber y) g) (⋯.monodromy γ e)) = ↑(((hp.toPermFiber y) g) (⋯.monodromy γ' e))

Tactic:
eq

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

Goal state before:
pp: c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ ↑z.re + ↑c.im * I ∈ ball c r

Tactic:
by
  suffices dist (z.re + c.im * I) c ≤ dist z c from lt_of_le_of_lt this hz
  rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
    Real.sq_sqrt (by positivity)]
  simp [sq_nonneg _]

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

Goal state before:
pp: case pos.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ 0 = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Tactic:
simp only [h0, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ne_eq, true_and, ofReal_eq_zero]

Goal state after:
case pos.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ ¬1 - z = 0 ∨ sSupNormIm f 1 = 0 ∧ ¬z = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
⊢ z / (↑u - ↑l) - ↑l / (↑u - ↑l) ∈ verticalClosedStrip 0 1

Tactic:
by
  simp only [verticalClosedStrip, Complex.div_re, mem_preimage, sub_re, mem_Icc,
    sub_nonneg, tsub_le_iff_right, ofReal_re, ofReal_im, sub_im, sub_self, mul_zero, zero_div,
    add_zero]
  simp only [verticalClosedStrip] at hz
  norm_cast
  simp_rw [Complex.normSq_ofReal, mul_div_assoc, div_mul_eq_div_div_swap,
    div_self (by linarith : u - l ≠ 0), ← div_eq_mul_one_div]
  constructor
  · gcongr
    exact hz.1
  · rw [← sub_le_sub_iff_right (l / (u - l)), add_sub_assoc, sub_self, add_zero, div_sub_div_same,
      div_le_one (by simp [hul]), sub_le_sub_iff_right l]
    exact hz.2

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
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
have hμ0' : μ s ≠ 0 := by
    have hμ : μ s = μ (Ι a b) := by rw [measure_congr hs_ev]
    rwa [hμ]

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
hμ0' : μ s ≠ 0
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c |R| = circleAverage f c R

Tactic:
by
  by_cases! hR : 0 ≤ R
  · rw [abs_of_nonneg hR]
  · rw [abs_of_neg hR, circleAverage_neg_radius]

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
x : ℂ
hx : x ∈ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|}
⊢ ‖x - c‖ ≤ |R|

Tactic:
exact hx.2

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case inr
⊢ Filter.Tendsto (fun x ↦ x * log x) (𝓝 0) (𝓝 0)

Tactic:
mul_comm _ (log _)

Goal state after:
case inr
⊢ Filter.Tendsto (fun x ↦ log x * x) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ max C C'

Tactic:
rcases hexp with ⟨c, hc, B, hO⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ ‖f z‖ ≤ max C C'
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: case right.e_6
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ)
⊢ log ((starRingEnd ℂ) (g x)) + log (g x) = (starRingEnd ℂ) (log (g x)) + log (g x)

Tactic:
rw [← Complex.log_conj]

Goal state after:
case right.e_6.h
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ)
⊢ (g x).arg ≠ Real.pi
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: x : ℝ
⊢ sinc (-x) = sinc x

Tactic:
by
  by_cases hx : x = 0
  · simp [hx]
  · simp [sinc_of_ne_zero hx, sinc_of_ne_zero (neg_ne_zero.mpr hx)]

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

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hR : 0 < R
hw : 0 ∈ ball 0 R
z : ℂ
hz : z ∈ sphere 0 |R|
⊢ ((z + 0) / (z - 0)).re • f z = f z

Tactic:
abs_of_pos hR

Goal state after:
case inr.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hR : 0 < R
hw : 0 ∈ ball 0 R
z : ℂ
hz : z ∈ sphere 0 R
⊢ ((z + 0) / (z - 0)).re • f z = f z
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ 0 < (↑x).re

Tactic:
rw [Complex.ofReal_re]

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ 0 < x
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: R : ℝ
w c : ℂ
hw : w ∈ ball c R
⊢ ∃ d > 0, ball w d ⊆ ball c R ∧ ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖

Tactic:
by
  have : Disjoint {w} (ball c R)ᶜ := by simpa
  obtain ⟨d, hd, h_disj⟩ := this.exists_thickenings isCompact_singleton isOpen_ball.isClosed_compl
  refine ⟨d, hd, ?_, ?_⟩ <;> grw [thickening_singleton] at h_disj
  · simpa using (h_disj.mono_right (self_subset_thickening hd _)).subset_compl_left
  · intro x hx θ
    have := h_disj.subset_compl_right hx
    simp only [mem_compl_iff, mem_thickening_iff, mem_ball, not_lt, not_exists, not_and] at this
    simpa [← dist_eq_norm'] using this (circleMap c R θ) (by simp [dist_eq_norm, le_abs_self])

Goal state after: