mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹

Tactic:
suffices ∫ t in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹ by
    simp_rw [deriv_inv_log, neg_div, intervalIntegral.integral_neg] at this
    linarith

Goal state after:
a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (t : ℝ) in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
hR : 0 ≤ R
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) c R

Tactic:
exact hf.circleIntegrable_posLog_norm

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

Goal state before:
pp: h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝[≠] 0)

Tactic:
refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_
    (.of_forall fun q ↦ exp_ne_zero _)
  rw [tendsto_zero_iff_norm_tendsto_zero]
  simp only [norm_qParam]
  apply (tendsto_comap'_iff (m := fun y ↦ Real.exp (-2 * π * y / h)) (range_im ▸ univ_mem)).mpr
  refine Real.tendsto_exp_atBot.comp (.atBot_div_const hh (tendsto_id.const_mul_atTop_of_neg ?_))
  simpa using Real.pi_pos

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
m : ℤ
hm : invQParam h (𝕢 h z) = z + ↑m * ↑h
⊢ cuspFunction h f (𝕢 h z) = f z

Tactic:
simpa only [this, hm] using hf.int_mul m z

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := ⋯
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < ↑n + 2
⊢ R - ‖w‖ < R * (↑n + 2)

Tactic:
calc R - ‖w‖
      _ ≤ R * 1 := by aesop
      _ < R * (n + 2) := by gcongr; grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: ⊢ ∫ (x : ℝ) in -1..1, √(1 - x ^ 2) = ∫ (x : ℝ) in sin (-(π / 2))..sin (π / 2), √(1 - x ^ 2)

Tactic:
by rw [sin_neg, sin_pi_div_two]

Goal state after:
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ k → ↑(Ioo (-1) 1)

pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMono ?refine_1

pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) ?refine_1

Tactic:
· refine codRestrict (fun x ↦ x / (1 + |x|)) _ fun x ↦ abs_lt.1 ?_
    have H : 0 < 1 + |x| := (abs_nonneg x).trans_lt (lt_one_add _)
    calc
      |x / (1 + |x|)| = |x| / (1 + |x|) := by rw [abs_div, abs_of_pos H]
      _ < 1 := (div_lt_one H).2 (lt_one_add _)

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMono (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_2.refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMonoOn (fun x ↦ x / (1 + |x|)) (Ici 0)

Tactic:
· rintro x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy
      simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff₀, hx.trans_lt (lt_one_add _),
        hy.trans_lt (lt_one_add _), *]

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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
this : (∑ᶠ (a : ℂ), ↑((divisor f (closedBall c |r|)) a)) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
← le_div_iff₀

Goal state after:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
this : ∑ᶠ (a : ℂ), ↑((divisor f (closedBall c |r|)) a) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
this : (∑ᶠ (a : ℂ), ↑((divisor f (closedBall c |r|)) a)) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
⊢ 0 < Real.log (R / r)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 * ↑g 1 0 ^ 2 = -(↑g).det

Tactic:
dist_eq_norm,

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ ‖↑z - -↑(↑g 1 1) / ↑(↑g 1 0)‖ ^ 2 * ↑g 1 0 ^ 2 = -(↑g).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : (↑(cd 0) * z + ↑(cd 1)).im = Complex.im 0
⊢ cd 0 = 0

Tactic:
simpa only [Complex.add_im, Complex.mul_im, Complex.ofReal_im, zero_mul, add_zero,
      Complex.zero_im, mul_eq_zero, hz, or_false] using! h

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
⊢ ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖

Tactic:
intro n

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
⊢ dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n

Tactic:
intro n

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inl
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : ↑g 0 0 + ↑g 1 1 = 0
hb : ↑g 0 1 = ↑g 1 0
⊢ False

Tactic:
← Matrix.trace_fin_two

Goal state after:
case mp.inl
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : (↑g).trace = 0
hb : ↑g 0 1 = ↑g 1 0
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ ↑(g • z) = num g ↑z / denom g ↑z

Tactic:
change smulAux' g z = _

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ smulAux' g ↑z = num g ↑z / denom g ↑z
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
by
  rcases K.eq_empty_or_nonempty with rfl | hne
  · exact ⟨1, 1, Real.zero_lt_one, empty_subset _⟩
  obtain ⟨u, _, hu⟩ := hK.exists_isMaxOn hne (_root_.continuous_abs.comp continuous_re).continuousOn
  obtain ⟨v, _, hv⟩ := hK.exists_isMinOn hne continuous_im.continuousOn
  exact ⟨|re u|, im v, v.im_pos, fun k hk ↦ ⟨isMaxOn_iff.mp hu _ hk, isMinOn_iff.mp hv _ hk⟩⟩

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

Goal state before:
pp: case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0

Tactic:
← hg

Goal state after:
case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = m
hm0 : m ≠ 0
hmsq : ↑g ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
⊢ ∃ i ∈ s, f i = 0

Tactic:
have : ∃ᶠ τ in 𝓝[≠] I, ∏ i ∈ s, f i τ = 0 := .of_forall <| by simpa using congrFun h0

Goal state after:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
this : ∃ᶠ (τ : ℍ) in 𝓝[≠] I, ∏ i ∈ s, f i τ = 0
⊢ ∃ i ∈ s, f i = 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
by_cases h : FiniteDimensional K L
  swap
  · rw [norm_eq_one_of_not_module_finite h]
    by_cases hx : IsIntegral K x
    · have h₁ : ¬ FiniteDimensional K⟮x⟯ L := fun H ↦ h <| by
        have : FiniteDimensional K K⟮x⟯ := adjoin.finiteDimensional hx
        exact Finite.trans K⟮x⟯ L
      simp [finrank_of_not_finite h₁]
    · rw [norm_eq_one_of_not_module_finite]
      · simp
      · refine fun H ↦ hx ?_
        rw [← isIntegral_gen]
        exact IsIntegral.isIntegral (gen K x)
  let F := K⟮x⟯
  nth_rw 1 [← coe_gen K x]
  rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow,
    finrank_eq_card_chooseBasisIndex]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]
  apply eq_inv_of_mul_eq_one_left
  rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel_right]
  exact add_nonneg zero_le_one (sq_nonneg _)

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist x c

Tactic:
dist_inversion_center

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ R ^ 2 / dist x c = R ^ 2 / dist x c
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ R ^ 2 / (dist x c * dist (inversion c R y) c) * dist x (inversion c R y) * dist x c =
    dist x (inversion c R y) * dist y c

Tactic:
dist_inversion_center

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + - -cexp (-x)) * 2⁻¹

Tactic:
neg_neg

Goal state after:
case e'_9
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x)) * 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
⊢ deriv (iteratedDeriv n cosh) = iteratedDeriv (n + 1) cosh

Tactic:
iteratedDeriv_succ

Goal state after:
case succ
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
⊢ deriv (iteratedDeriv n cosh) = deriv (iteratedDeriv n cosh)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
⊢ deriv (iteratedDeriv n sinh) = iteratedDeriv (n + 1) sinh

Tactic:
iteratedDeriv_succ

Goal state after:
case succ
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
⊢ deriv (iteratedDeriv n sinh) = deriv (iteratedDeriv n sinh)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|

Tactic:
simp only [← _root_.abs_mul, Real.dist_eq]

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ |z.im - w.im * ((z.im / w.im + w.im / z.im) / 2)| = |w.im * ((z.im / w.im - w.im / z.im) / 2)|
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' sphere z r = sphere (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
ext w; constructor
  · rintro ⟨w, hw, rfl⟩
    exact dist_eq_iff_dist_coe_center_eq.1 hw
  · intro hw
    lift w to ℍ using im_pos_of_dist_center_le (sphere_subset_closedBall hw)
    exact mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r

pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card

Tactic:
· fun_prop

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ log⁺ ‖f θ - a₀‖ ≤ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ + log 2

Tactic:
convert! posLog_norm_add_le (-f θ) a₀ using 2

Goal state after:
case e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ ‖f θ - a₀‖ = ‖-f θ + a₀‖

case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ = log⁺ ‖-f θ‖ + log⁺ ‖a₀‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
this :
  ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺ ≤ ∫ (x : ℝ) in Ioc 0 (2 * π), log⁺ ‖f (circleMap 0 R β)‖ + log 2
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)

Tactic:
integral_const,

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
this :
  ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺ ≤
    (volume.restrict (Ioc 0 (2 * π))).real univ • (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ logCounting D ℓ < |logCounting D (1 + ℓ)|

Tactic:
abs_of_nonneg (logCounting_nonneg h (by grind))

Goal state after:
case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ logCounting D ℓ < logCounting D (1 + ℓ)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
hEq : ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K
r : ℝ
hr₁ : logCounting D' r = ↑N * log r - K
hr₂ : 1 ≤ r
⊢ ‖logCounting D r‖ ≤ C * ‖log r‖ → (↑N - C) * log r ≤ K

Tactic:
hr₃

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
hEq : ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K
r : ℝ
hr₁ : logCounting D' r = ↑N * log r - K
hr₂ : 1 ≤ r
hr₃ : ‖logCounting D r‖ ≤ C * ‖log r‖
⊢ (↑N - C) * log r ≤ K
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
zy : z ≤ y
u : ℝ
xu : x ≤ u
uz : u ≤ z
v : ℝ
xv : x ≤ v
vz : v ≤ z
⊢ eVariationOn f (Icc u v) = eVariationOn f (Icc u (min y v))

Tactic:
inf_of_le_right (vz.trans zy)

Goal state after:
case inl.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
zy : z ≤ y
u : ℝ
xu : x ≤ u
uz : u ≤ z
v : ℝ
xv : x ≤ v
vz : v ≤ z
⊢ eVariationOn f (Icc u v) = eVariationOn f (Icc u v)
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_1.refine_1.cons
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) →
    Pairwise (Wbtw R head) tail → List.Wbtw R tail → Pairwise (Sbtw R head) tail
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: head2 :: tail)
hp : Pairwise (Wbtw R head) (head2 :: tail)
ht : List.Wbtw R (head2 :: tail)
⊢ Pairwise (Sbtw R head) (head2 :: tail)

Tactic:
rw [pairwise_cons] at hp hpne hpne ⊢
          refine ⟨fun a ha ↦ ⟨hp.1 a ha, ?_⟩, ?_⟩
          · refine ⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩
            simp
          · rw [wbtw_cons] at ht
            grind [List.pairwise_iff_forall_sublist]

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #s' ≤ #(s'.biUnion fun a' ↦ t ↑a')

Tactic:
← card_image_of_injective s' Subtype.coe_injective

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #(image (fun a ↦ ↑a) s') ≤ #(s'.biUnion fun a' ↦ t ↑a')
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
Nat.add_one

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x