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
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm)) ⟨e₀, he⟩ =
    cov.monodromy (Path.Homotopic.Quotient.mk ((pγ'.map ⋯).trans (pγ'.map ⋯).symm)) ⟨e₀, he⟩

Tactic:
conv_rhs => rw [← eq.2 ⟨.reflTransSymm _⟩, mk_refl, monodromy_refl]

Goal state after:
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
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm)) ⟨e₀, he⟩ = id ⟨e₀, he⟩
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: 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)
a : A
⊢ F' a ∈ p ⁻¹' s

Tactic:
rw [Set.mem_preimage, hF'₂]; exact (f a).2

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
hM1_one : ¬1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))

Tactic:
· apply le_trans _ (le_max_left _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_one_of_one_le_of_nonpos
        hM1_one (Right.neg_nonpos_iff.mpr hset.1)]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
hM1_one : ¬1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
h : IsExactOn f s
x₀ : ℂ
y : E
⊢ ∃ g, g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x

Tactic:
obtain ⟨η, hη⟩ := h
  use fun z ↦ η z - η x₀ + y, by simp, by simpa using hη

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

Goal state before:
pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e

Tactic:
simp only [one_mul, add_sub_cancel, hz₂]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ∀ b_1 ∈ norm ∘ f '' re ⁻¹' {1}, b_1 ≤ b

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ (norm ∘ f '' re ⁻¹' {1}).Nonempty

Tactic:
· simpa [comp_apply, mem_image, forall_exists_index,
          and_imp, forall_apply_eq_imp_iff₂] using hb

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ (norm ∘ f '' re ⁻¹' {1}).Nonempty
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re / (u - l) ≤ 1 + l / (u - l)

Tactic:
· rw [← sub_le_sub_iff_right (l / (u - l)), add_sub_assoc, sub_self, add_zero, div_sub_div_same,
      div_le_one (by simp [hul]), sub_le_sub_iff_right l]
    exact hz.2

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x

Tactic:
by
  constructor
  · exact h.1.continuousLinearMap_comp l
  · filter_upwards [h.1.laplacian_CLM_comp_left_nhds (l := l), h.2]
    simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ circleAverage f c R = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z

Tactic:
by
  calc circleAverage f c R
  _ = (↑(2 * π) : ℂ)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) := by
    simp [circleAverage, ← coe_smul]
  _ = (2 * π * I)⁻¹ • ∫ θ in 0..2 * π, I • f (circleMap c R θ) := by
    rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
    match_scalars
    field
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) := by
    unfold circleIntegral
    congr with θ
    simp [deriv_circleMap, circleMap_sub_center, smul_smul]
    field_simp [circleMap_ne_center h]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
⊢ 0 ≤ circleAverage f c R

Tactic:
by_cases hf : CircleIntegrable f c R
  · rw [← circleAverage_const 0 c |R|, circleAverage, circleAverage, smul_eq_mul, smul_eq_mul,
      mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]
    apply intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos)
      intervalIntegrable_const hf (fun θ _ ↦ h₂f (circleMap c R θ) (circleMap_mem_sphere' c R θ))
  · rw [circleAverage.integral_undef hf]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ‖f z‖ ≤ C

Tactic:
by
  obtain ⟨z, rfl⟩ : ∃ z', z' * I = z := ⟨z / I, div_mul_cancel₀ _ I_ne_zero⟩
  simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im
  change ‖(f ∘ (· * I)) z‖ ≤ C
  have H : MapsTo (· * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using! hw.symm
  rcases hB with ⟨c, hc, B, hO⟩
  refine quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him
    (fun x hx => ?_) hz_im hz_re
  · simpa only [Function.comp_def, norm_mul, norm_I, mul_one]
      using hO.comp_tendsto ((tendsto_mul_right_cobounded I_ne_zero).inf H.tendsto)
  · rw [comp_apply, mul_assoc, I_mul_I, mul_neg_one, ← ofReal_neg]
    exact hre _ (neg_nonpos.2 hx)

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

Goal state before:
pp: ⊢ -1 + ↑1 = 0

Tactic:
Int.cast_one,

Goal state after:
⊢ -1 + 1 = 0
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key : (-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))).re ≤ R * r
⊢ R ^ 2 + r ^ 2 - 2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re ≤ R ^ 2 + r ^ 2 + 2 * (R * r)

Tactic:
by rw [sub_eq_add_neg, ← mul_neg, ← neg_re]; gcongr

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ sinc x ≤ |x|⁻¹

Tactic:
by
  rw [sinc_of_ne_zero hx]
  exact sin_div_le_inv_abs x

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

Goal state before:
pp: n : ℕ
⊢ log⁺ ↑n = log ↑n

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ log⁺ ↑n = log ↑n

case neg
n : ℕ
hn : ¬n = 0
⊢ log⁺ ↑n = log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: n : ℕ
x : ℝ
⊢ log⁺ (x ^ n) = ↑n * log⁺ x

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
n : ℕ
x : ℝ
hn : n = 0
⊢ log⁺ (x ^ n) = ↑n * log⁺ x

case neg
n : ℕ
x : ℝ
hn : ¬n = 0
⊢ log⁺ (x ^ n) = ↑n * log⁺ x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x = 2 - 2 * cos x

Tactic:
sin_sq_add_cos_sq

Goal state after:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 1 + 1 - 2 * cos x = 2 - 2 * cos x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
neg_div,

Goal state after:
a b : ℝ
ha : 1 < a
hb : 1 < b
this : ∫ (t : ℝ) in a..b, -(t⁻¹ / log t ^ 2) = (log b)⁻¹ - (log a)⁻¹
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
⊢ circleAverage (fun x ↦ log ‖x + a‖) 0 1 = log⁺ ‖a‖

Tactic:
by
  have : (log ‖· + a‖) = (log ‖· - -a‖) := by simp
  simp [this]

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

Goal state before:
pp: case h
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ Set.univ ∈ nhds z ∧ (Set.univ ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite

Tactic:
simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]

Goal state after:
case h
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ (sphere 0 1 \ {z | ¬z + (↑R)⁻¹ * (c - a) = 0}).Finite
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 : E
hz : z ∈ sphere 0 1
t : ℂ
ht : t ∈ ball 0 r
⊢ ray z t ∈ ball z₀ r

Tactic:
by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using! ht

Goal state after:
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:
by simpa [zero_pow (NeZero.ne n)] using h.symm

Goal state after:
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 : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
n : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
θ : ℝ
h : ¬‖circleMap 0 R θ - ρ‖ = 0
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ

Tactic:
apply norm_herglotzLogIntegrand_circleMap_le hR hρ (by positivity) (by linarith) hn
        (hr_lt n).le

Goal state after:
ρ 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 : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
θ : ℝ
h : ¬‖circleMap 0 R θ - ρ‖ = 0
⊢ 0 < ‖circleMap 0 R θ - ρ‖
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:
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₁⟩

Goal state after:
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
r' : ℝ
hr' : r' < r
hr'₀ : 0 < r'
hzr' : z ∈ Metric.ball c r'
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
⊢ ∑ᶠ (u : ℂ), ↑(D u) * (log R - log ‖c - u‖) = ∑ᶠ (u : ℂ), ↑(D u) * log (R * ‖c - u‖⁻¹) + ↑(D c) * log R

Tactic:
by_cases h : c ∈ D.support

Goal state after:
case pos
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
⊢ ∑ᶠ (u : ℂ), ↑(D u) * (log R - log ‖c - u‖) = ∑ᶠ (u : ℂ), ↑(D u) * log (R * ‖c - u‖⁻¹) + ↑(D c) * log R

case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∉ Function.support D
⊢ ∑ᶠ (u : ℂ), ↑(D u) * (log R - log ‖c - u‖) = ∑ᶠ (u : ℂ), ↑(D u) * log (R * ‖c - u‖⁻¹) + ↑(D c) * log R
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

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

Tactic:
neg_div,

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

Goal state before:
pp: case refine_1
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 / r)

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

Tactic:
by_cases hf : ‖f‖ = 0; · exact ⟨0, by aesop⟩
  have := Metric.instTietzeExtensionClosedBall.{u, v} 𝕜 (0 : E) (by simp_all : 0 < ‖f‖)
  have hf' x : f x ∈ Metric.closedBall 0 ‖f‖ := by simpa using! f.norm_coe_le_norm x
  obtain ⟨g, hg_mem, hg⟩ := (f : C(s, E)).exists_forall_mem_restrict_eq hs hf'
  simp only [Metric.mem_closedBall, dist_zero_right] at hg_mem
  let g' : X →ᵇ E := .ofNormedAddCommGroup g (map_continuous g) ‖f‖ hg_mem
  refine ⟨g', ?_, by ext x; congrm($(hg) x)⟩
  apply le_antisymm ((g'.norm_le <| by positivity).mpr hg_mem)
  refine (f.norm_le <| by positivity).mpr fun x ↦ ?_
  have hx : f x = g' x := by simpa using! congr($(hg) x).symm
  rw [hx]
  exact g'.norm_le (norm_nonneg g') |>.mp le_rfl x

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁸ : TopologicalSpace X₁
X : Type u
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormalSpace X
s✝ : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁵ : TopologicalSpace Y✝
inst✝⁴ : TietzeExtension Y✝
ι : Type u_1
Y : ι → Type v
inst✝³ : (i : ι) → TopologicalSpace (Y i)
inst✝² : ∀ (i : ι), TietzeExtension (Y i)
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, (i : ι) → Y i)
g' : (x : ι) → C(X✝, Y x)
hg' : ∀ (x : ι), ContinuousMap.restrict s (g' x) = (ContinuousMap.piEquiv (↑s) Y).symm f x
⊢ ContinuousMap.restrict s ((ContinuousMap.piEquiv X✝ Y) g') = f

Tactic:
ext x i; congrm($(hg' i) x)

Goal state after:
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) = r.comp (ι.comp f)
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x

Tactic:
← r.comp_assoc ι,

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) = (r.comp ι).comp f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: u : ℝˣ
z : ℍ
⊢ (GeneralLinearGroup.scalar (Fin 2)) u • z = z

Tactic:
glPos_smul_def

Goal state after:
u : ℝˣ
z : ℍ
⊢ { coe := num ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z / denom ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z,
      coe_im_pos := ⋯ } =
    z

case hg
u : ℝˣ
z : ℍ
⊢ 0 < ↑(GeneralLinearGroup.det ((GeneralLinearGroup.scalar (Fin 2)) u))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
n : ℤ
⊢ ModularGroup.T ^ n • z = ↑n +ᵥ z

Tactic:
rw [UpperHalfPlane.ext_iff, coe_vadd, add_comm, coe_specialLinearGroup_apply]
  simp [ModularGroup.coe_T_zpow,
    of_apply, cons_val_zero, Complex.ofReal_one, one_mul, cons_val_one,
    zero_mul, zero_add, div_one]

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

Goal state before:
pp: a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ (fun x ↦ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x ↦ b * a +ᵥ x) ∘ fun x ↦ ⟨a * a, ⋯⟩ • x

Tactic:
ext1 ⟨z, hz⟩

Goal state after:
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • { coe := z, coe_im_pos := hz } =
    ((fun x ↦ b * a +ᵥ x) ∘ fun x ↦ ⟨a * a, ⋯⟩ • x) { coe := z, coe_im_pos := hz }
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGL ⟨!![a, b; c, d], ⋯⟩) ↑z ≠ 0
hc : c ≠ 0
⊢ (fun x ↦ ⟨!![a, b; c, d], ⋯⟩ • x) =
    (fun x ↦ a / c +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ c * d +ᵥ x) ∘ fun x ↦ ⟨c * c, ⋯⟩ • x

Tactic:
ext1 ⟨z, hz⟩

Goal state after:
case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGL ⟨!![a, b; c, d], ⋯⟩) ↑z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; c, d], ⋯⟩ • { coe := z, coe_im_pos := hz } =
    ((fun x ↦ a / c +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ c * d +ᵥ x) ∘ fun x ↦ ⟨c * c, ⋯⟩ • x)
      { coe := z, coe_im_pos := hz }
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ (trace ℝ ℂ) z = 2 * z.re

Tactic:
rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex,
    Matrix.trace_fin_two]

Goal state after:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 + !![z.re, -z.im; z.im, z.re] 1 1 = 2 * z.re
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inl
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
b : ℝ
hb : IsLUB (range ⇑f) b
g dg : Y →ᵇ ℝ
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
ha : IsGLB (range ⇑f) (g y)
hmem : ∀ (x : X), f x ∈ Icc (g y) b
hle : g y ≤ b
hlt : g y < b
c : ℝ := (g y + b) / 2
hac : g y < c
hcb : c < b
hsub : c - g y = b - c
hg_mem : ∀ (y_1 : Y), g y_1 ∈ Icc (g y) b
ha' : ¬∃ x, f x = g y
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {g y})
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - g y)) (⇑g ⁻¹' {g y})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - g y)
⊢ g y < (g + dg) y

Tactic:
refine (lt_add_iff_pos_right _).2 ?_
        calc
          0 < c - g y := sub_pos.2 hac
          _ = dg y := (dga rfl).symm

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
⊢ ∃ x, (g + dg) y ∈ Icc (f x) b

Tactic:
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)

Goal state after:
case inr
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
hay : a < (g + dg) y
⊢ ∃ x, (g + dg) y ∈ Icc (f x) b