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

Goal state before:
pp: case inr.inr.inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this : ∀ {C : ℝ}, (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → 0 < C → ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ 0 < C'

Tactic:
· refine ((norm_nonneg (f (a * I))).trans (hle_a _ ?_)).trans_lt hC'
      rw [mul_I_im, ofReal_re]

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

Goal state before:
pp: case convert_8
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
⊢ ContinuousWithinAt (fun ε ↦ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖) (Ioi 0) 0

Tactic:
simp_rw [← ofReal_add]
      have : ∀ 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 : ℂ)‖ := by
              intro x hx
              simp only [norm_mul]
              repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
              · simp only [sub_re, one_re]
              · simpa using (ne_comm.mpr (ne_of_lt hz.1))
              · simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))
      apply tendsto_nhdsWithin_congr this _
      simp only [zero_add]
      rw [norm_mul, norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,
        norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _]
      · apply Tendsto.mul
        · apply Tendsto.rpow_const
          · nth_rw 2 [← zero_add (sSupNormIm f 0)]
            exact Tendsto.add_const (sSupNormIm f 0) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))
          · right; simp only [sub_nonneg, le_of_lt hz.2]
        · apply Tendsto.rpow_const
          · nth_rw 2 [← zero_add (sSupNormIm f 1)]
            exact Tendsto.add_const (sSupNormIm f 1) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))
          · right; simp only [le_of_lt hz.1]
      · simpa using (ne_comm.mpr (ne_of_lt hz.1))
      · simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))

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

Goal state before:
pp: case left
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
⊢ ContDiffAt ℝ 2 (⇑l ∘ f) x

pp: case right
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
⊢ Δ (⇑l ∘ f) =ᶠ[𝓝 x] 0

Tactic:
· exact h.1.continuousLinearMap_comp l

Goal state after:
case right
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
⊢ Δ (⇑l ∘ f) =ᶠ[𝓝 x] 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
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ insert x s
⊢ (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y

Tactic:
s.insert_eq_of_mem hx

Goal state after:
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
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ s
⊢ (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y
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₁ : ContDiffAt ℝ 2 f₁ x
h₂ : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] Δ f₁ + Δ f₂

Tactic:
by
  filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp)] with x h₁x h₂x
  exact h₁x.laplacian_add h₂x

Goal state after:
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
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ insert x s
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y

Tactic:
s.insert_eq_of_mem hx

Goal state after:
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
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ s
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst✝ : CompleteSpace E
⊢ circleAverage f c 0 = f c

Tactic:
circleAverage

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst✝ : CompleteSpace E
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c 0 θ) = f c
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
⊢ circleAverage f c R = a

Tactic:
circleAverage

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
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) = a
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ Function.Injective fun x ↦ x • z

Tactic:
by
  rintro ⟨x, hx⟩ ⟨y, hy⟩ h
  simp_all [UpperHalfPlane.ext_iff, ne_zero]

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

Goal state before:
pp: c w z : ℂ
⊢ herglotzRieszKernel c w (z + c) = herglotzRieszKernel 0 (w - c) z

Tactic:
simp [herglotzRieszKernel_fun_def]

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

Goal state before:
pp: ⊢ ¬ContinuousAt (fun x ↦ log (log x)) 0

Tactic:
by
  suffices Tendsto (fun x ↦ log (log x)) (nhdsWithin 0 {0}ᶜ) (cobounded ℝ) from
    not_continuousAt_of_tendsto this nhdsWithin_le_nhds (disjoint_nhds_cobounded _)
  have : Tendsto log atBot atTop := by
    convert tendsto_log_atTop.comp tendsto_neg_atBot_atTop; ext; simp
  exact (this.mono_right atTop_le_cobounded).comp tendsto_log_nhdsNE_zero

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

Goal state before:
pp: case inr.inl
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ deriv (fun x ↦ log (log x)) (-1) = (-1)⁻¹ / log (-1)

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt continuousAt ‹_›)]

Goal state after:
case inr.inl
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ 0 = (-1)⁻¹ / log (-1)
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: case inr.inr.inl
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ deriv (fun x ↦ log (log x)) 0 = 0⁻¹ / log 0

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt continuousAt ‹_›)]

Goal state after:
case inr.inr.inl
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ 0 = 0⁻¹ / log 0
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: case inr.inr.inr
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ deriv (fun x ↦ log (log x)) 1 = 1⁻¹ / log 1

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt continuousAt ‹_›)]

Goal state after:
case inr.inr.inr
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ 0 = 1⁻¹ / log 1
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case neg.inr.refine_2.inr.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ μ (Icc c 0) < ⊤

Tactic:
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_Icc

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

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)

Tactic:
have hr : r + 1 ≠ 0 := by
    rcases h with h | h
    · apply_fun Complex.re
      rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne, add_eq_zero_iff_eq_neg]
      exact h.ne'
    · rw [Ne, ← add_eq_zero_iff_eq_neg] at h; exact h.1

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ ∫ (x : ℝ) in 0..2 * π, log (4 * sin (x / 2) ^ 2) / 2 = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2)

Tactic:
have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring

Goal state after:
this : ∀ {x : ℝ}, x / 2 = 2⁻¹ * x
⊢ ∫ (x : ℝ) in 0..2 * π, log (4 * sin (x / 2) ^ 2) / 2 = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: this✝ : AnalyticOnNhd ℝ (fun x ↦ 4 * sin x ^ 2) Set.univ
this : 4 * sin (π / 2) ^ 2 ≠ 0 → (fun x ↦ 4 * sin x ^ 2) ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ {x | (fun x ↦ (fun x ↦ log (4 * sin x ^ 2)) x = (fun x ↦ log 4 + 2 * log (sin x)) x) x} ∈ codiscreteWithin Set.univ

Tactic:
simp only [sin_pi_div_two, one_pow, mul_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      Set.preimage_compl, forall_const] at this

Goal state after:
this✝ : AnalyticOnNhd ℝ (fun x ↦ 4 * sin x ^ 2) Set.univ
this : ((fun x ↦ 4 * sin x ^ 2) ⁻¹' {0})ᶜ ∈ codiscrete ℝ
⊢ {x | (fun x ↦ (fun x ↦ log (4 * sin x ^ 2)) x = (fun x ↦ log 4 + 2 * log (sin x)) x) x} ∈ codiscreteWithin Set.univ
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

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

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

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
⊢ (∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀) ∨ 𝓝 (f z₀) ≤ map f (𝓝 z₀)

Tactic:
refine or_iff_not_imp_left.mpr fun h => ?_

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
⊢ 𝓝 (f z₀) ≤ map f (𝓝 z₀)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ ↑h * (z / ↑h) + ↑h * ↑m = z + ↑m * ↑h

Tactic:
mul_div_cancel₀ _ (mod_cast hh),

Goal state after:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ z + ↑h * ↑m = z + ↑m * ↑h
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = c

Tactic:
by
  obtain ⟨z₀, _⟩ := h₂U.nonempty
  by_contra h₅
  grind [not_isOpen_singleton (c₀ : ℝ), (by aesop : (re '' f '' U) = { c₀ }), isOpenMap_re
    (f '' U) ((h₁f.is_constant_or_isOpen h₂U.isPreconnected).resolve_left h₅ U (by tauto) h₁U)]

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

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ n =
    C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n - cos x ^ (n + 2)

Tactic:
simp [sin_sq, sub_mul, ← pow_add, add_comm]

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ (fun z ↦ f z - cuspFunction h f 0) =O[I∞] fun z ↦ rexp (-2 * π * z.im / h)

Tactic:
simpa [comp_def, eq_cuspFunction hh.ne' hf, norm_qParam] using
    differentiableAt_cuspFunction_zero hh hf h_hol h_bd |>.isBigO_sub.mono
      nhdsWithin_le_nhds |>.comp_tendsto (qParam_tendsto hh) |>.norm_right

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

Goal state before:
pp: ⊢ ∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - sin x ^ 2) * cos x = ∫ (x : ℝ) in -(π / 2)..π / 2, cos x ^ 2

Tactic:
refine integral_congr_ae (MeasureTheory.ae_of_all _ fun _ h => ?_)
          rw [uIoc_of_le (neg_le_self (le_of_lt (half_pos Real.pi_pos))), Set.mem_Ioc] at h
          rw [← Real.cos_eq_sqrt_one_sub_sin_sq (le_of_lt h.1) h.2, pow_two]

Goal state after:
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
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
have hf₀ : ∀ z ∈ U, f z ≠ 0 := by
    intro z hz hfz
    simpa [hfz, (ne_of_mem_of_not_mem hz hU₀).symm] using hf_inv z

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
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
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
hR : ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
g : GL n R
⊢ ∃ r, r ^ Fintype.card n * GeneralLinearGroup.det g = 1

Tactic:
obtain ⟨r, hr⟩ := hR g.det⁻¹
    exact ⟨r, by simpa [mul_eq_one_iff_eq_inv] using hr⟩

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.refine_2
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)
⊢ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_

Goal state after:
case inr.refine_2
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
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.refine_2.inr.inr
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‖ / 3 ≤ f x
hle₂ : ‖f‖ / 3 ≤ f x
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

Tactic:
calc
          |g (e x) - f x| = f x - ‖f‖ / 3 := by
            rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
              abs_of_nonneg (sub_nonneg.2 hle₂)]
          _ ≤ 2 / 3 * ‖f‖ := by linarith

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))
⊢ ⇑(const Y ((a + b) / 2) + g) ∘ e = ⇑f

Tactic:
· ext x
    have : g (e x) = f x - (a + b) / 2 := congr_fun hge x
    simp [this]

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

Goal state before:
pp: n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex) z

Tactic:
by
  rw [contMDiffAt_iff]
  constructor
  · -- continuity at z
    rw [ContinuousAt, nhds_induced, tendsto_comap_iff]
    refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_
    simpa [ofComplex_apply_of_im_pos hz] using! tendsto_id
  · -- smoothness in local chart
    simpa using! contDiffAt_id.congr_of_eventuallyEq (eventuallyEq_coe_comp_ofComplex hz)

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

Goal state before:
pp: case refine_2
z✝ w✝ : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
w : ℍ
hw : w ∈ ball z (log (R / z.im + 1))
⊢ rexp (dist w z) - 1 < R / z.im

Tactic:
sub_lt_iff_lt_add,

Goal state after:
case refine_2
z✝ w✝ : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
w : ℍ
hw : w ∈ ball z (log (R / z.im + 1))
⊢ rexp (dist w z) < R / z.im + 1
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
⊢ ∃ t₃ ∈ ultrafilterBasis α, u ∈ t₃ ∧ t₃ ⊆ (fun s ↦ {u | s ∈ u}) a ∩ (fun s ↦ {u | s ∈ u}) b

Tactic:
refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩ <;> apply mem_of_superset hv

Goal state after:
case refine_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ a

case refine_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ b
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 *
      arsinh
        (dist (-(↑y₁)⁻¹) (-(↑y₂)⁻¹) /
          (2 * √({ coe := -(↑y₁)⁻¹, coe_im_pos := ⋯ }.im * { coe := -(↑y₂)⁻¹, coe_im_pos := ⋯ }.im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
dist_neg_neg,

Goal state after:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 *
      arsinh
        (dist (↑y₁)⁻¹ (↑y₂)⁻¹ /
          (2 * √({ coe := -(↑y₁)⁻¹, coe_im_pos := ⋯ }.im * { coe := -(↑y₂)⁻¹, coe_im_pos := ⋯ }.im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 * arsinh (dist ↑y₁ ↑y₂ / (‖↑y₁‖ * ‖↑y₂‖) / (2 * √(- -(y₁.im / normSq ↑y₁) * - -(y₂.im / normSq ↑y₂)))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
neg_neg,

Goal state after:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 * arsinh (dist ↑y₁ ↑y₂ / (‖↑y₁‖ * ‖↑y₂‖) / (2 * √(y₁.im / normSq ↑y₁ * (y₂.im / normSq ↑y₂)))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
⊢ { down := ∞ } ∈ g ⁻¹' s

Tactic:
have : Filter.Tendsto (@OnePoint.some ℕ) Filter.atTop (𝓝 ∞) := by
    rw [← Nat.cofinite_eq_atTop, ← cocompact_eq_cofinite, ← coclosedCompact_eq_cocompact]
    exact tendsto_coe_infty

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ { down := ∞ } ∈ g ⁻¹' s
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 x✝¹) (𝓝 x✝)

Tactic:
specializes_coe

Goal state after:
case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ x✝¹ ⤳ x✝ ∨ Disjoint (𝓝 x✝¹) (𝓝 x✝)