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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
z : ℂ
⊢ z ∈ sphere 0 |1| → (fun x ↦ log ‖x - a‖) z = (fun x ↦ log ‖1 - x⁻¹ * a‖) z

Tactic:
hz

Goal state after:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ (fun x ↦ log ‖x - a‖) z = (fun x ↦ log ‖1 - x⁻¹ * a‖) z
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
⊢ 0 < z.re → f z = 0

Tactic:
hz

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
⊢ f z = 0
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z✝ : ℂ
hz : 0 < z✝.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
z : ℂ
⊢ 1 ≤ ‖z‖ → ‖expR z.re ^ n * expR (B * ‖z‖ ^ c)‖ ≤ ‖expR ((↑n + max B 0) * ‖z‖ ^ max c 1)‖

Tactic:
hz

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z✝ : ℂ
hz✝ : 0 < z✝.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : 1 ≤ ‖z‖
⊢ ‖expR z.re ^ n * expR (B * ‖z‖ ^ c)‖ ≤ ‖expR ((↑n + max B 0) * ‖z‖ ^ max c 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
⊢ 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Tactic:
hz

Goal state after:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Tactic:
convert!
        (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const
          (2 * (t + 1)) using 1

Goal state after:
case e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ z ^ t / 2 = (t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ z ∈ sphere 0 |1| → ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite

Tactic:
hz

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
z : ℂ
⊢ ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0 → log ‖↑R * (z + ↑R⁻¹ * (c - a))‖ = log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖

Tactic:
hz

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
z : ℂ
hz : ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0
⊢ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖ = log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: k : ℕ
⊢ 0 < π

Tactic:
simp [pi_pos]

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

Goal state before:
pp: k : ℕ
⊢ 0 < 2

Tactic:
simp [pi_pos]

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
⊢ z ∈ (derivative P).rootSet ℂ → z ∈ (convexHull ℝ) (P.rootSet ℂ)

Tactic:
hz

Goal state after:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : z ∈ (derivative P).rootSet ℂ
⊢ z ∈ (convexHull ℝ) (P.rootSet ℂ)
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: q : ℤ[X]
this : q.natDegree = 0
p : ℤ[X]
h : ∀ (z : ℂ), ¬((aeval z) (q * p) = 0 ∧ (aeval z) (q * p).mirror = 0)
hq' : q ∣ (q * p).mirror
hp : IsUnit q.leadingCoeff
⊢ IsUnit q

Tactic:
eq_C_of_natDegree_eq_zero this,

Goal state after:
q : ℤ[X]
this : q.natDegree = 0
p : ℤ[X]
h : ∀ (z : ℂ), ¬((aeval z) (q * p) = 0 ∧ (aeval z) (q * p).mirror = 0)
hq' : q ∣ (q * p).mirror
hp : IsUnit q.leadingCoeff
⊢ IsUnit (C (q.coeff 0))
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 : (map (algebraMap ℤ ℂ) q).IsRoot z
⊢ False

Tactic:
rw [IsRoot, eval_map_algebraMap] at hz

Goal state after:
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
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
have hr_tendsto : Tendsto r atTop (nhds R) :=
    sub_zero R ▸ (tendsto_const_nhds.sub <| tendsto_const_nhds.div_atTop <|
      tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop)

Goal state after:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
z : ℂ
⊢ z ∈ U → f z ≠ 0

Tactic:
hz

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
z : ℂ
hz : z ∈ U
⊢ f z ≠ 0
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
⊢ z ∈ U → HasStrictDerivAt f (2 * f z)⁻¹ z

Tactic:
hz

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ HasStrictDerivAt f (2 * f z)⁻¹ z
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 : ℂ
⊢ z ∈ U → (fun z ↦ ↑ε / (f z - x)) z ∈ ball 0 1

Tactic:
hz

Goal state after:
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
⊢ (fun z ↦ ↑ε / (f z - x)) z ∈ ball 0 1
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 : ℂ
⊢ z ∈ U → ∀ ⦃x₂ : ℂ⦄, x₂ ∈ U → (fun z ↦ ↑ε / (f z - x)) z = (fun z ↦ ↑ε / (f z - x)) x₂ → z = x₂

Tactic:
hz

Goal state after:
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
⊢ ∀ ⦃x₂ : ℂ⦄, x₂ ∈ U → (fun z ↦ ↑ε / (f z - x)) z = (fun z ↦ ↑ε / (f z - x)) x₂ → z = x₂
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 : ℂ
⊢ z ∈ U → deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0

Tactic:
hz

Goal state after:
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
⊢ deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0
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 : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
⊢ (divisor f CB) x = 0 x

Tactic:
by_cases h : x ∈ CB

Goal state after:
case pos
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 = ⊤
x : ℂ
h : x ∈ CB
⊢ (divisor f CB) x = 0 x

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 = ⊤
x : ℂ
h : x ∉ CB
⊢ (divisor f CB) x = 0 x
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 : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
z : ℂ
⊢ f z = 0 z → log ‖f z‖ = 0 z

Tactic:
hz

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 : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
z : ℂ
hz : f z = 0 z
⊢ log ‖f z‖ = 0 z
Module: Mathlib.Analysis.RCLike.Sqrt

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

Tactic:
cpow_inv_two_im_eq_neg_sqrt (by simp),

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

Goal state before:
pp: case pos
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
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f

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
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f

Tactic:
· exact ⟨0, by aesop⟩

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
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE (num g z / denom g z)).im = |↑(GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)

Tactic:
abs_of_nonpos (not_lt.mp h)

Goal state after:
case neg
g : GL (Fin 2) ℝ
z : ℂ
h : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE (num g z / denom g z)).im = -↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: h : IsCompact univ
⊢ IsCompact (Complex.im ⁻¹' Ioi 0)

Tactic:
simpa [isEmbedding_coe.isCompact_iff] using! h

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

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

Tactic:
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.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℍ
h : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ -↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z) =
    |↑(GeneralLinearGroup.det g)| * (↑z).im / Complex.normSq (denom g ↑z)

Tactic:
abs_of_nonpos (not_lt.mp h)

Goal state after:
case neg
g : GL (Fin 2) ℝ
z : ℍ
h : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ -↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z) =
    -↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: z : ℂ
⊢ z ∈ Complex.im ⁻¹' Set.Ioi 0 → z.im = (↑ofComplex z).im

Tactic:
hz

Goal state after:
z : ℂ
hz : z ∈ Complex.im ⁻¹' Set.Ioi 0
⊢ z.im = (↑ofComplex z).im
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ (norm R) ((norm S) a) = (norm R) a

Tactic:
norm_apply S,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ (norm R) (LinearMap.det ((lmul S A) a)) = (norm R) a
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ (num g / denom g) ∘ UpperHalfPlane.coe =ᶠ[𝓝 τ] (fun z ↦ ↑(g • ↑ofComplex z)) ∘ UpperHalfPlane.coe

Tactic:
simp [Function.comp_def, coe_smul_of_det_pos hg]

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

Goal state before:
pp: x : ℝ
⊢ |0| < |x| ↔ x ≠ 0

Tactic:
by simp only [_root_.abs_zero, abs_pos]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

Tactic:
preStoneCechUnit,

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : Quot.mk (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : Quot.mk (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

Tactic:
preStoneCechUnit,

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : Quot.mk (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) = Quot.mk (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure b)
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : NoncompactSpace X
⊢ (𝓝[≠] ∞).NeBot

Tactic:
rw [nhdsNE_infty_eq]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : NoncompactSpace X
⊢ (map some (coclosedCompact X)).NeBot
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
by
    have h : IsProperMap (Prod.map f (fun x : X ↦ x)) := f_clemb.isProperMap.prodMap isProperMap_id
    have : (fun hx : H × X ↦ (hx.1 • hx.2, hx.2)) = (fun hx ↦ (f hx.1 • hx.2, hx.2)) := by
      simp [f_compat]
    rw [this]
    exact ProperSMul.isProperMap_smul_pair.comp h

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
⊢ IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
have hU : IsCompact U := hK.image continuous_fst

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
⊢ IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ IsCompact (f ⁻¹' Uᶜ)

Tactic:
rw [hf.isCompact_iff, image_preimage_eq_iff.mpr (by simpa [hy])]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ IsCompact Uᶜ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x * f₂ x‖) 0 r

Tactic:
apply MeromorphicOn.circleIntegrable_posLog_norm

Goal state after:
case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ MeromorphicOn (fun x ↦ f₁ x * f₂ x) (sphere 0 |r|)
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: 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
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r

Tactic:
apply MeromorphicOn.circleIntegrable_posLog_norm

Goal state after:
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
⊢ MeromorphicOn (fun x ↦ f x - a₀) (sphere 0 |r|)
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

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

Tactic:
rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]

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

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0 = meromorphicTrailingCoeffAt f 0

Tactic:
rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]

Goal state after:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (fun x ↦ a) 0
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l

Tactic:
by
  rintro x hx y hy; cases hs hx hy
  rw [eVariationOn.subsingleton f (fun y hy z hz => hs hy.1 hz.1 : (s ∩ Icc x x).Subsingleton)]
  simp only [sub_self, mul_zero, ENNReal.ofReal_zero]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ (LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)) →
    HasConstantSpeedOnWith f s l

Tactic:
rw [hasConstantSpeedOnWith_iff_ordered]
    rintro h x xs y ys xy
    rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]

Goal state after: