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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (closedBall c |R|)]
    (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (closedBall c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ circleAverage ((∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (closedBall c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖) c R =
    circleAverage ((∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f CB) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖) c R

Tactic:
]

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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ log ‖g c‖ = log ‖g c‖

pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∀ u ∈ closedBall c |R|, g u ≠ 0

Tactic:
]

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∀ u ∈ closedBall c |R|, g u ≠ 0
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
⊢ |x| / (1 + |x|) = |x| / (1 + |x|)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: a : ℂ
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

Tactic:
]

Goal state after:
a : ℂ
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log (R * ‖c - u‖⁻¹) + ↑((divisor f CB) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log (R * ‖c - u‖⁻¹) + ↑((divisor f CB) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) a).sqrt else ↑√(re a)) =
    (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) a).sqrt else ↑√(re a)) =
    (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ¬∃ u, meromorphicOrderAt f ↑u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
]

Goal state after:
case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ¬∃ u, meromorphicOrderAt f ↑u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : I = 0
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)‖ + ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).im then 1 else -1) *
            ↑√((‖(map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)‖ - ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).re) / 2) *
          Complex.I) =
    ↑√((‖↑(re a) + ↑(im a) * I‖ + re (↑(re a) + ↑(im a) * I)) / 2) +
      (if 0 ≤ im (↑(re a) + ↑(im a) * I) then 1 else -1) *
          ↑√((‖↑(re a) + ↑(im a) * I‖ - re (↑(re a) + ↑(im a) * I)) / 2) *
        I

Tactic:
]

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : I = 0
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)‖ + ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).im then 1 else -1) *
            ↑√((‖(map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)‖ - ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).re) / 2) *
          Complex.I) =
    ↑√((‖↑(re a) + ↑(im a) * I‖ + re (↑(re a) + ↑(im a) * I)) / 2) +
      (if 0 ≤ im (↑(re a) + ↑(im a) * I) then 1 else -1) *
          ↑√((‖↑(re a) + ↑(im a) * I‖ - re (↑(re a) + ↑(im a) * I)) / 2) *
        I
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this : divisor f CB = 0
⊢ circleAverage (fun x ↦ log ‖f x‖) c R = 0

Tactic:
]

Goal state after:
case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this : divisor f CB = 0
⊢ circleAverage (fun x ↦ log ‖f x‖) c R = 0
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑√α + ↑(↑α).sqrt.im * I = ↑√α

Tactic:
]

Goal state after:
α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑√α + ↑(↑α).sqrt.im * I = ↑√α
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ circleAverage 0 c R = 0

pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0

Tactic:
]

Goal state after:
case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ circleAverage 0 c R = 0

c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ ↑√((complexRingEquiv h) a).re = (complexRingEquiv h) ↑√(re a)

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ ↑√((complexRingEquiv h) a).re = (complexRingEquiv h) ↑√(re a)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ (-↑α).sqrt = I * ↑√(↑α).re

Tactic:
]

Goal state after:
α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ (-↑α).sqrt = I * ↑√(↑α).re
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑(-↑α).sqrt.re + ↑(-↑α).sqrt.im * I = I * ↑√α

Tactic:
]

Goal state after:
α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑(-↑α).sqrt.re + ↑(-↑α).sqrt.im * I = I * ↑√α
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ Complex.I * ((complexRingEquiv h) a).sqrt = (complexRingEquiv h) (I * sqrt a)

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ Complex.I * ((complexRingEquiv h) a).sqrt = (complexRingEquiv h) (I * sqrt a)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast 0).untop₀ * Real.log R +
      Real.log ‖f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖

Tactic:
]

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast 0).untop₀ * Real.log R +
      Real.log ‖f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: ⊢ ↑√((‖I‖ + I.re) / 2) + ↑√((‖I‖ - I.re) / 2) * I = ↑√2⁻¹ * (1 + I)

Tactic:
]

Goal state after:
⊢ ↑√((‖I‖ + I.re) / 2) + ↑√((‖I‖ - I.re) / 2) * I = ↑√2⁻¹ * (1 + I)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: ⊢ ↑√((‖-I‖ + (-I).re) / 2) + ↑(-√((‖-I‖ - (-I).re) / 2)) * I = ↑√2⁻¹ * (1 - I)

Tactic:
]

Goal state after:
⊢ ↑√((‖-I‖ + (-I).re) / 2) + ↑(-√((‖-I‖ - (-I).re) / 2)) * I = ↑√2⁻¹ * (1 - I)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt else ↑√(re I)) = ↑√2⁻¹ * (1 - I) * I

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt else ↑√(re I)) = ↑√2⁻¹ * (1 - I) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) (-I)).sqrt else ↑√(re (-I))) =
    ↑√2⁻¹ * (1 + I) * -I

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) (-I)).sqrt else ↑√(re (-I))) =
    ↑√2⁻¹ * (1 + I) * -I
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 (M / ‖f c‖) / Real.log (R / r)
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

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‖)
⊢ 0 < Real.log (R / r)

Tactic:
]

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

Goal state before:
pp: ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ 1 / 2 ≤ ξ.im

Tactic:
]

Goal state after:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ 1 / 2 ≤ ξ.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case refine_2
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|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)

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

Goal state before:
pp: ⊢ TietzeExtension ↑(Metric.closedBall 2⁻¹ 2⁻¹)

Tactic:
]

Goal state after:
⊢ TietzeExtension ↑(Metric.closedBall 2⁻¹ 2⁻¹)
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: case neg
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
x : ↑s
hx : f x = g' ↑x
⊢ ‖g' ↑x‖ ≤ ‖g'‖

Tactic:
]

Goal state after:
case neg
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
x : ↑s
hx : f x = g' ↑x
⊢ ‖g' ↑x‖ ≤ ‖g'‖
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case pos
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|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u = c
⊢ ↑(ENat.map Nat.cast 0).untop₀ * Real.log (R / r) ≤ ↑(ENat.map Nat.cast 0).untop₀ * Real.log (R * ‖c - c‖⁻¹)

Tactic:
]

Goal state after:
case pos
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|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u = c
⊢ ↑(ENat.map Nat.cast 0).untop₀ * Real.log (R / r) ≤ ↑(ENat.map Nat.cast 0).untop₀ * Real.log (R * ‖c - c‖⁻¹)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
⊢ g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (GL n R)

Tactic:
]

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
u : Rˣ
⊢ (GeneralLinearGroup.scalar n) u ∈ (GeneralLinearGroup.scalar n).range

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
u : Rˣ
⊢ (GeneralLinearGroup.scalar n) u ∈ (GeneralLinearGroup.scalar n).range
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : ↑s
this : r.comp (ContinuousMap.restrict s g) = f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x

Tactic:
]

Goal state after:
case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : ↑s
this : r.comp (ContinuousMap.restrict s g) = f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ f.comp (GeneralLinearGroup.scalar n) = 1

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ f.comp (GeneralLinearGroup.scalar n) = 1
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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
⊢ -‖f‖ / 3 < ‖f‖ / 3

Tactic:
]

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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
⊢ -‖f‖ / 3 < ‖f‖ / 3
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.charpoly.coeff 1 ^ 2 - 4 * A.charpoly.coeff 0 * A.charpoly.coeff 2 = A.trace ^ 2 - 4 * A.det

Tactic:
]

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.charpoly.coeff 1 ^ 2 - 4 * A.charpoly.coeff 0 * A.charpoly.coeff 2 = A.trace ^ 2 - 4 * A.det
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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : f x ≤ -‖f‖ / 3
⊢ -‖f‖ / 3 - f x = -‖f‖ / 3 - f x

Tactic:
]

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|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ Real.log (M / ‖f c‖) = Real.log (M / ‖f c‖)

Tactic:
]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔ (σ g).toAlgEquiv (num g ↑z) = (σ g).toAlgEquiv ((σ g) ↑w * denom g ↑z)

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔ (σ g).toAlgEquiv (num g ↑z) = (σ g).toAlgEquiv ((σ g) ↑w * denom g ↑z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)
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).det / ↑g 1 0 ^ 2

Tactic:
]

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 ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2