mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ Tendsto (fun x ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
    (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))

Tactic:
apply intervalIntegral.tendsto_integral_filter_of_dominated_convergence bound

Goal state after:
case hF_meas
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (fun x ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) (volume.restrict (uIoc 0 (2 * π)))

case h_bound
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ False

Tactic:
refine h z ⟨?_, ?_⟩

Goal state after:
case refine_1
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p = 0

case refine_2
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p.mirror = 0
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
w : ℂ
hw : w ∈ U
heq : (fun z ↦ ↑ε / (f z - x)) z = (fun z ↦ ↑ε / (f z - x)) w
⊢ z = w

Tactic:
simpa [div_eq_mul_inv, hε₀.ne', hf_inj.eq_iff] using heq

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ((starRingEnd ℂ) z) =
    (starRingEnd ℂ) ((if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
y : ℝ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑y = ↑y

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z) =
    z

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ ((if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z).im ≠ 0 ↔ z.im ≠ 0

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℂ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det h) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z) =
    (if 0 < ↑(GeneralLinearGroup.det h) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ ‖(if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z‖ = ‖z‖

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : m.IsElliptic
hc : m 0 1 * m 1 0 = 0
⊢ False

Tactic:
rw [IsElliptic, discr_fin_two, trace_fin_two, det_fin_two, hc] at hm

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ ↑(-g • z) = ↑(g • z)

Tactic:
simp [coe_smul]

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
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
⊢ ∃ g, (∀ (y : Y), ∃ x, g y ∈ Icc (f x) b) ∧ ⇑g ∘ e = ⇑f

Tactic:
by
    rcases exists_extension_forall_mem_Icc_of_isClosedEmbedding f hmem hle he with ⟨g, hg_mem, hgf⟩
    -- If `a ∈ range f`, then we are done.
    rcases em (∃ x, f x = a) with (⟨x, rfl⟩ | ha')
    · exact ⟨g, fun y => ⟨x, hg_mem _⟩, hgf⟩
    /- Otherwise, `g ⁻¹' {a}` is disjoint with `range e ∪ g ⁻¹' (Ici c)`, hence there exists a
        function `dg : Y → ℝ` such that `dg ∘ e = 0`, `dg y = 0` whenever `c ≤ g y`, `dg y = c - a`
        whenever `g y = a`, and `0 ≤ dg y ≤ c - a` for all `y`. -/
    have hd : Disjoint (range e ∪ g ⁻¹' Ici c) (g ⁻¹' {a}) := by
      refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩
      · rw [Set.disjoint_left]
        rintro _ ⟨x, rfl⟩ (rfl : g (e x) = a)
        exact ha' ⟨x, (congr_fun hgf x).symm⟩
      · exact Set.disjoint_singleton_right.2 hac.not_ge
    rcases exists_bounded_mem_Icc_of_closed_of_le
        (he.isClosed_range.union <| isClosed_Ici.preimage g.continuous)
        (isClosed_singleton.preimage g.continuous) hd (sub_nonneg.2 hac.le) with
      ⟨dg, dg0, dga, dgmem⟩
    replace hgf : ∀ x, (g + dg) (e x) = f x := by
      intro x
      simp [dg0 (Or.inl <| mem_range_self _), ← hgf]
    refine ⟨g + dg, fun y => ?_, funext hgf⟩
    have hay : a < (g + dg) y := by
      rcases (hg_mem y).1.eq_or_lt with (rfl | hlt)
      · refine (lt_add_iff_pos_right _).2 ?_
        calc
          0 < c - g y := sub_pos.2 hac
          _ = dg y := (dga rfl).symm
      · exact hlt.trans_le (le_add_of_nonneg_right (dgmem y).1)
    rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩
    refine ⟨x, hxy.le, ?_⟩
    rcases le_total c (g y) with hc | hc
    · simp [dg0 (Or.inr hc), (hg_mem y).2]
    · calc
        g y + dg y ≤ c + (c - a) := add_le_add hc (dgmem _).2
        _ = b := by rw [hsub, add_sub_cancel]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case zero
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = 0
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
rw [Fintype.card_eq_zero_iff] at l
    simp_rw [Matrix.det_isEmpty, map_one, det_one]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto (↑ofComplex) (𝓝 z) (𝓝 (↑ofComplex z))

Tactic:
nhds_induced,

Goal state after:
case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto (↑ofComplex) (𝓝 z) (comap UpperHalfPlane.coe (𝓝 ↑(↑ofComplex z)))
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
this : (f' M'.det).det = ((comp m m n n R[X]) (M'.map ⇑f')).det
⊢ eval 0 ((comp m m n n R[X]) (M'.map ⇑f')).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
eval_zero_comp_det

Goal state after:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
this : (f' M'.det).det = ((comp m m n n R[X]) (M'.map ⇑f')).det
⊢ ((comp m m n n R) (M.map ⇑f)).det = ((comp m m n n R) (M.map ⇑f)).det
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 : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x

Tactic:
rw [inversion, div_self, one_pow, one_smul, vsub_vadd]
    rwa [dist_ne_zero]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℍ
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ

Tactic:
wlog hg : 0 < g.det.val generalizing g

Goal state after:
case inr
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ

τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
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 : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ ((R / (R ^ 2 / dist x c)) ^ 2 * (R / dist x c) ^ 2) • (x -ᵥ c) +ᵥ c = x

Tactic:
← mul_pow,

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 : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ (R / (R ^ 2 / dist x c) * (R / dist x c)) ^ 2 • (x -ᵥ c) +ᵥ c = x
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 : ℝ
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
by_cases hR : R = 0 <;> simp [inversion_eq_center, hR]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist z w ≤ dist ↑z ↑w / √(z.im * w.im)

Tactic:
rw [dist_le_iff_le_sinh, ← div_mul_eq_div_div_swap, self_le_sinh_iff]

Goal state after:
z w : ℍ
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv cosh x

Tactic:
by
    rw [interior_Ici, mem_Ioi] at hx; rwa [deriv_cosh, sinh_pos_iff]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous[_, inst✝¹] g₁
h₂ : Continuous[_, inst✝¹] g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ g₁ = g₂

Tactic:
apply h₁.ext_on denseRange_stoneCechUnit h₂
  rintro _ ⟨x, rfl⟩
  exact congr_fun h x

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
⊢ stoneCechExtend hg ∘ stoneCechUnit = g

Tactic:
by
  ext x
  rw [stoneCechExtend, Function.comp_apply, stoneCechUnit, T2Quotient.lift_mk]
  apply congrFun (preStoneCechExtend_extends hg)

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
hf : Continuous f
⊢ Continuous (proximity f ⊤)

Tactic:
simp only [proximity, reduceDIte]
  fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: 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₀‖

Tactic:
← norm_neg

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₀‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
refine (circleIntegrable_congr fun a ha ↦ ?_).2 (circleIntegrable_const
      (log ‖meromorphicTrailingCoeffAt f 0‖) 0 1)

Goal state after:
case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖ = log ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
by_cases h: ¬MeromorphicAt f 0
  · have {a : ℂ} : ¬MeromorphicAt (fun x ↦ f x - a) 0 := by
      rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
    simp_all
  rcases lt_trichotomy (meromorphicOrderAt f 0) 0 with hneg | hzero | hpos
  · refine (circleIntegrable_congr fun a ha ↦ ?_).2 (circleIntegrable_const
      (log ‖meromorphicTrailingCoeffAt f 0‖) 0 1)
    rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]
    rw [meromorphicOrderAt_const]
    aesop
  · apply CircleIntegrable.congr_codiscreteWithin
     (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero (not_not.1 h) hzero)
    simpa [norm_sub_rev] using circleIntegrable_log_norm_sub_const 1
  · apply (circleIntegrable_congr _).2 (circleIntegrable_const 0 0 1)
    exact fun _ ↦ log_trailingCoeff_eq_zero_on_unitSphere hpos

Goal state after:
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)⁺
⊢ Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ

Tactic:
have : CircleIntegrable (log⁺ ‖f ·‖) 0 R := h.meromorphicOn.circleIntegrable_posLog_norm

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)⁺
this : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 R
⊢ Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: 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 ≤ ℓ
⊢ 1 ≤ ℓ

Tactic:
simp [ℓ]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
A : E → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), {x | s x < d} = ⋃ f ∈ A d, U f d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)

Tactic:
set 𝓕' := ⋃ d ∈ D, A d

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
A : E → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), {x | s x < d} = ⋃ f ∈ A d, U f d
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
⊢ D = 0 ↔ logCounting D =O[atTop] 1

Tactic:
refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
this : ∀ (z : E), 0 ≤ ↑(((toClosedBall r) f) z) * log (r * ‖z‖⁻¹)
⊢ 0 ≤ ↑(f 0)

Tactic:
simpa using h 0

Goal state after:
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
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
· rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
      rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
        hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu,
        inf_of_le_right (vz.trans zy)]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ : ℝ
⊢ id x✝ = x✝ - 0 + φ 0

Tactic:
have : φ 0 = 0 := by
    have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self]
    obtain ⟨x, xs, hx⟩ := hm
    apply le_antisymm ((φm ⟨le_rfl, hs⟩ xs xs.1).trans_eq hx) _
    have := φst ▸ mapsTo_image φ (Icc 0 s)
    exact (mem_Icc.mp (@this 0 (by rw [mem_Icc]; exact ⟨le_rfl, hs⟩))).1

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ : ℝ
this : φ 0 = 0
⊢ id x✝ = x✝ - 0 + φ 0
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
ht : ¬tail = []
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail

Tactic:
rw [wbtw_cons] at h

Goal state after:
case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
ht : ¬tail = []
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail
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:
rw [← card_image_of_injective s' Subtype.coe_injective]
    convert! ht (s'.image fun z => z.1) using 1
    apply congr_arg
    ext y
    simp

Goal state after: