mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
F' : C(A, E)
hF'₁ : F' a₀ = ↑(F a₀)
hF'₂ : ∀ (x : A), p (F' x) = ↑(f x)
x✝ : A
⊢ ↑((s.restrictPreimage p ∘ ⇑{ toFun := fun a ↦ ⟨F' a, ⋯⟩, continuous_toFun := ⋯ }) x✝) = ↑(f x✝)

Tactic:
simp [← hF'₂]

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
g : Gᵐᵒᵖ
e' : ↑(p ⁻¹' {x}) := ⟨MulOpposite.unop g • ↑e, ⋯⟩
he' : e' = ⟨MulOpposite.unop g • ↑e, ⋯⟩
⊢ ∃ a, (hp.fundamentalGroupToMulOpposite e) a = g

Tactic:
set Γ : Path (e : E) (e' : E) :=
    { toFun := PathConnectedSpace.somePath (e : E) (e' : E)
      continuous_toFun := by fun_prop
      source' := by simp
      target' := by simp }

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
g : Gᵐᵒᵖ
e' : ↑(p ⁻¹' {x}) := ⟨MulOpposite.unop g • ↑e, ⋯⟩
he' : e' = ⟨MulOpposite.unop g • ↑e, ⋯⟩
Γ : Path ↑e ↑e' := { toFun := ⇑(PathConnectedSpace.somePath ↑e ↑e'), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ ∃ a, (hp.fundamentalGroupToMulOpposite e) a = g
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2

Tactic:
cases mem_uIoc.mp y_in_I <;> nlinarith

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ‖f z‖ ≤ ‖interpStrip f z‖

Tactic:
apply tendsto_le_of_eventuallyLE _ _ (eventuallyle f z hB hd hz)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ Tendsto (fun x ↦ ‖f z‖) (𝓝[>] 0) (𝓝 ‖f z‖)

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ Tendsto (fun ε ↦ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖) (𝓝[>] 0) (𝓝 ‖interpStrip f z‖)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖↑(x + sSupNormIm f 0) ^ (1 - z)‖ * ‖↑(x + sSupNormIm f 1) ^ z‖

Tactic:
norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * ‖↑(x + sSupNormIm f 1) ^ z‖

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (1 - z).re ≠ 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * ‖↑(x + sSupNormIm f 1) ^ z‖

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (1 - z).re ≠ 0

Tactic:
norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ z.re ≠ 0

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (1 - z).re ≠ 0
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
this : Tendsto (fun R ↦ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C

Tactic:
filter_upwards [this.eventually (ge_mem_nhds hC₀), hA] with R hR Hle w hre him
      calc
        ‖g ε w • f w‖ ≤ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) := ?_
        _ ≤ C := hR
      rw [norm_smul, Real.exp_add, ← hre, Real.exp_add, Real.exp_log hA₀, mul_assoc, mul_comm _ A]
      gcongr
      exacts [hδ <| Ioo_subset_Icc_self him, Hle _ hre him]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ z.re ≠ 0

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (1 - z).re ≠ 0

Tactic:
norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ z.re ≠ 0

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ (1 - z).re ≠ 0
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x✝ : E
h : f₁ =ᶠ[𝓝 x✝] f₂
x : E
hx : iteratedFDeriv ℝ 2 f₁ x = iteratedFDeriv ℝ 2 f₂ x
⊢ Δ f₁ x = Δ f₂ x

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, hx]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl

Goal state before:
pp: case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closedBall x r)

Tactic:
rw [← closure_ball x hr]

Goal state after:
case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
θ : ℝ
| f (circleMap c R θ)

Tactic:
rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
θ : ℝ
| a
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x : ℝ
hx : 1 ≤ |x|
⊢ 0 ≤ log |x|

Tactic:
apply log_nonneg hx

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ ∑ t ∈ s, |f t| ∈ Set.Ici 0

Tactic:
by simp [Finset.sum_nonneg]

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

Goal state before:
pp: case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c ↦ ↑c ^ (r + 1) / (r + 1)) [[0, c]]

Tactic:
refine ((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn

Goal state after:
case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ 0 < (r + 1).re
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u = ⊤
this : (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (Ι a b)] 0
⊢ IntervalIntegrable 0 volume a b

Tactic:
apply Iff.mpr _root_.intervalIntegrable_const_iff

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u = ⊤
this : (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (Ι a b)] 0
⊢ Real.zero✝ = 0 ∨ volume (Ι a b) < ⊤
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case pos
r : ℝ
hr : r = 0
⊢ 2 * ↑(sin r) = 2 * ↑r * ↑(sinc r)

Tactic:
simp [hr]

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

Goal state before:
pp: a b c : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, (c ^ 2)⁻¹ * (1 + (x / c) ^ 2)⁻¹ = c⁻¹ * (arctan (b / c) - arctan (a / c))

Tactic:
by
    simp [integral_comp_div (fun x => (c ^ 2)⁻¹ * (1 + x ^ 2)⁻¹) hc]
    field_simp

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

Goal state before:
pp: case inr.inl
a : ℂ
h : 1 = ‖a‖
⊢ log⁺ ‖a‖ = 0

Tactic:
posLog_eq_zero_iff

Goal state after:
case inr.inl
a : ℂ
h : 1 = ‖a‖
⊢ |‖a‖| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case inr.inr
a : ℂ
h : ‖a‖ < 1
⊢ log⁺ ‖a‖ = 0

Tactic:
posLog_eq_zero_iff

Goal state after:
case inr.inr
a : ℂ
h : ‖a‖ < 1
⊢ |‖a‖| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
rw [← ofReal_inj]

Goal state after:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) =
    ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1)))
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
h : circleMap 0 r θ = w
⊢ False

Tactic:
grind [norm_circleMap_zero, lt_of_le_of_lt (Complex.norm_nonneg w) hwr]

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

Goal state before:
pp: w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
h : circleMap 0 r θ = ρ
⊢ False

Tactic:
grind [norm_circleMap_zero, lt_of_le_of_lt (Complex.norm_nonneg w) hwr]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
⊢ ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)

Tactic:
refine fun z hz t ht => AnalyticAt.comp ?_ ?_

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
z : E
hz : z ∈ sphere 0 1
t : ℂ
ht : t ∈ ball 0 r
⊢ AnalyticAt ℂ g (ray z t)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
z : E
hz : z ∈ sphere 0 1
t : ℂ
ht : t ∈ ball 0 r
⊢ AnalyticAt ℂ (ray z) t
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
z : { z // z ≠ 0 }
h : (fun x ↦ x ^ n) 0 = ↑z
⊢ ↑z = 0

Tactic:
simpa [zero_pow (NeZero.ne n)] using h.symm

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
by
  obtain ⟨r', hr', hr'₀, hzr'⟩ : ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r' := by
    obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)
    exact ⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩
  lift r' to NNReal using hr'₀.le
  have hz' : z - c ∈ Metric.eball 0 r' := by
    rw [Metric.eball_coe]
    simpa only [mem_ball_iff_norm, sub_zero] using hzr'
  have H := (hf.mono <| Metric.closedBall_subset_ball hr').hasFPowerSeriesOnBall hr'₀
      |>.hasSum_iteratedFDeriv hz'
  simp only [add_sub_cancel] at H
  convert H with n
  simpa only [iteratedDeriv_eq_iteratedFDeriv, smul_eq_mul, mul_one, Finset.prod_const,
    Finset.card_fin]
    using ((iteratedFDeriv ℂ n f c).map_smul_univ (fun _ ↦ z - c) (fun _ ↦ 1)).symm

Goal state after:
Module: Mathlib.Order.Monotone.Odd

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ -f y < -f x

Tactic:
← h₁,

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < -f x
Module: Mathlib.Order.Monotone.Odd

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ -f y ≤ -f x

Tactic:
← h₁,

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ f (-y) ≤ -f x
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : ℝ
⊢ re (sqrt ↑a) = √a

Tactic:
aesop (add simp [sqrt, Complex.re_sqrt_ofReal])

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

Goal state before:
pp: case neg
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 (analyticOrderAt f u)).untop₀ * Real.log |R / r| ≤
    ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀ * Real.log |R * ‖c - u‖⁻¹|

Tactic:
gcongr 2

Goal state after:
case ha
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
⊢ 0 ≤ ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀

case hxy
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
⊢ |R / r| ≤ |R * ‖c - u‖⁻¹|
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
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|
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (m - (scalar (Fin 2)) (m.trace / 2)) ^ 2 = (scalar (Fin 2)) (m.discr / 4)

Tactic:
simp only [scalar_apply, trace_fin_two, discr_fin_two, trace_fin_two,
    det_fin_two, sq, (by norm_num : (4 : K) = 2 * 2)]
  ext i j
  fin_cases i <;>
  fin_cases j <;>
  · simp [Matrix.mul_apply]
    field

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)
        (num g z / denom g z)).im =
    |↑(GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)

Tactic:
split_ifs with h <;>
  [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]] <;>
  simpa only [Complex.conjCAE_apply, Complex.star_def, Complex.conj_im,
    neg_mul, neg_div, neg_inj] using! moebius_im g z

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ m.IsParabolic ↔ ∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0

Tactic:
by
  constructor
  · exact fun hm ↦ ⟨_, _, (add_sub_cancel ..).symm, sub_ne_zero.mpr fun h ↦ hm.1 ⟨_, h.symm⟩,
      hm.sub_eigenvalue_sq_eq_zero⟩
  · rintro ⟨a, n, hm, hn0, hnsq⟩
    constructor
    · refine fun ⟨b, hb⟩ ↦ hn0 ?_
      rw [← sub_eq_iff_eq_add'] at hm
      simpa only [← hm, ← hb, ← map_sub, ← map_pow, ← map_zero (scalar (Fin 2)), scalar_inj,
        sq_eq_zero_iff] using hnsq
    · suffices scalar (Fin 2) (m.discr / 4) = 0 by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto
      rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]
      simp [mul_div_cancel_left₀ _ (NeZero.ne (2 : K)),
        (Matrix.isNilpotent_trace_of_isNilpotent ⟨2, hnsq⟩).eq_zero, hnsq]

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

Goal state before:
pp: ⊢ ContractibleSpace ℍ

Tactic:
rw [isEmbedding_coe.toHomeomorph.trans (.setCongr range_coe) |>.contractibleSpace_iff]

Goal state after:
⊢ ContractibleSpace ↑upperHalfPlaneSet
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ (g • z).im = |(num g ↑z / denom g ↑z).im|

Tactic:
change (smulAux' g z).im = _

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (smulAux' g ↑z).im = |(num g ↑z / denom g ↑z).im|