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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ B, f =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ B, g =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < a, ∃ B, (f - g) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)

Tactic:
have : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ →
      (fun z : ℂ => expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l]
        fun z => expR (B₂ * ‖z‖ ^ c₂) := fun hc hB₀ hB ↦ .of_norm_eventuallyLE <| by
    filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
    simp only [Real.norm_eq_abs, Real.abs_exp]
    gcongr

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ B, f =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ B, g =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
⊢ ∃ c < a, ∃ B, (f - g) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
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
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
X✝ Y✝ Z✝ : FundamentalGroupoid X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾cov.monodromy (x✝¹ ≫ x✝) = ↾cov.monodromy x✝¹ ≫ ↾cov.monodromy x✝

Tactic:
ext : 3; simpa using! cov.monodromy_trans_apply _ _ _

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h : meromorphicOrderAt f x = 0
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • g z
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
filter_upwards [h₃g] with z hz using by simpa using hz

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
⊢ log
      ‖((∏ᶠ (i : ℂ), canonicalFactor R i w ^ (divisor f B₀R) i) * ∏ᶠ (i : ℂ), (w - i) ^ (-divisor f S₀R) i) •
          meromorphicTrailingCoeffAt f w‖ =
    log
      ‖((∏ i ∈ t₂, canonicalFactor R i w ^ (divisor f B₀R) i) * ∏ i ∈ t₁, (w - i) ^ (-divisor f S₀R) i) •
          meromorphicTrailingCoeffAt f w‖

Tactic:
by
      rw [finprod_eq_prod_of_mulSupport_subset (s := t₂) _ _,
        finprod_eq_prod_of_mulSupport_subset (s := t₁) _ _]
      <;> simpa [ht₁, ht₂] using mulSupport_pow_subset_support ..

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 : ℂ
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
w : ℂ
hw : w.im ∈ Icc (a - b) (a + b)
⊢ |(aff w).im| ≤ d * b

Tactic:
← Real.closedBall_eq_Icc,

Goal state after:
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
w : ℂ
hw : w.im ∈ closedBall a b
⊢ |(aff w).im| ≤ d * b
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✝ : SimplyConnectedSpace E
⊢ Injective ⇑(hp.fundamentalGroupToMulOpposite e)

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, ker_fundamentalGroupToMulOpposite, MonoidHom.ker_eq_bot_iff]
  exact hp.monodromyPerm_injective

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

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

Tactic:
simp only [norm_mul, ← ofReal_add, norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _,
    sub_re, one_re]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
⊢ fderiv ℝ (⇑reCLM) (F y) ∘SL fderiv ℝ F y = fderiv ℝ f y

Tactic:
ContinuousLinearMap.fderiv,

Goal state after:
case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
⊢ reCLM ∘SL fderiv ℝ F y = fderiv ℝ f y
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := ⋯
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x✝ y : ℂ
hy : y ∈ univ
x : ℂ
⊢ (fderiv ℝ (⇑reCLM) (F y) ∘SL fderiv ℝ F y) x = (fderiv ℝ f y) (x.re • 1 + x.im • I)

pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := ⋯
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x✝ y : ℂ
hy : y ∈ univ
x : ℂ
⊢ (fderiv ℝ f y) (x.re • 1 + x.im • I) = (fderiv ℝ f y) x

Tactic:
· simp only [map_smul, map_add]
      simp [(h₁F y).hasFDerivAt.restrictScalars ℝ |>.fderiv, g]

Goal state after:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := ⋯
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x✝ y : ℂ
hy : y ∈ univ
x : ℂ
⊢ (fderiv ℝ f y) (x.re • 1 + x.im • I) = (fderiv ℝ f y) x
Module: Mathlib.Analysis.Complex.Poisson

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

Tactic:
exact herglotzRieszKernel_def c w z

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

Goal state before:
pp: case h₂
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ |f t_max| ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
rw [posLog_abs]

Goal state after:
case h₂
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (f t_max) ≤ ∑ t ∈ s, log⁺ (f t)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

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

Tactic:
rw [integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two,
    integral_log_sin_zero_pi_div_two]

Goal state after:
⊢ 2 * (-log 2 * π / 2) = -log 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
rw [← intervalIntegral.integral_congr (fun _ _ ↦ deriv_log_log_apply)]

Goal state after:
a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (x : ℝ) in a..b, deriv (fun x ↦ log (log x)) x = log (log b) - log (log a)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_3
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
n : ℕ
y : ℝ
⊢ ‖g n (↑y * I)‖ ≤ C

Tactic:
· rw [hg, re_ofReal_mul, I_re, mul_zero, Real.exp_zero, one_pow, one_mul]
    exact hC y

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

Goal state before:
pp: h : ℝ
hh : h ≠ 0
z : ℂ
⊢ ∃ m, invQParam h (𝕢 h z) = z + ↑m * ↑h

Tactic:
by
  dsimp only [qParam, invQParam]
  obtain ⟨m, hm⟩ := log_exp_exists (2 * ↑π * I * z / ↑h)
  refine ⟨m, by rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]⟩

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

Goal state before:
pp: case neg
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}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ¬∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
right
    simp only [not_forall] at h
    -- Otherwise, it is open along at least one direction and that implies the result
    obtain ⟨z, hz, hrz⟩ := h
    specialize h1 z hz 0 (mem_ball_self hr)
    have h7 := h1.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hrz
    rw [show gray z 0 = g z₀ by simp [gray, ray], ← map_compose] at h7
    refine h7.trans (map_mono ?_)
    have h10 : Continuous fun t : ℂ => z₀ + t • z := by fun_prop
    simpa using! h10.tendsto 0

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
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, y ∈ {0}ᶜ → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
this : DifferentiableOn ℂ (update (cuspFunction h f) 0 (cuspFunction h f 0)) S
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
update_eq_self

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, y ∈ {0}ᶜ → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
this : DifferentiableOn ℂ (cuspFunction h f) S
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
simpa using integral_sin_pow_mul_cos_pow_odd 1 0

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.im RCLike.I = 1
⊢ ((RCLike.map 𝕜 ℂ) a).sqrt = (RCLike.map 𝕜 ℂ) (RCLike.sqrt a)

Tactic:
aesop (add simp [RCLike.sqrt])

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

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
⊢ 0 ≤ r

Tactic:
by_contra! hr'

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : r < 0
⊢ False
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
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 : X
left✝ : a ≤ f x
hxy : f x < (g + dg) y
hc : g y ≤ c
⊢ c + (c - a) = b

Tactic:
hsub,

Goal state after:
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 : X
left✝ : a ≤ f x
hxy : f x < (g + dg) y
hc : g y ≤ c
⊢ c + (b - c) = b
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)

Tactic:
simp [field, cosh_dist, Complex.dist_eq, Complex.sq_norm, normSq_apply]
  ring

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

Goal state before:
pp: case refine_2
z✝ w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ 𝓝 z

Tactic:
nhds_induced

Goal state after:
case refine_2
z✝ w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 ↑z)
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
f : R →+* S
hf : Continuous[inst✝², inst✝] ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] ⇑(map f)

Tactic:
refine IsInducing.subtypeVal.continuous_iff.mpr ?_

Goal state after:
n : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
f : R →+* S
hf : Continuous[inst✝², inst✝] ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] (Subtype.val ∘ ⇑(map f))
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 * (-(↑y₂)⁻¹).im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
neg_im,

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 * -(↑y₂)⁻¹.im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
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)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : DiscreteTopology X
f : X → Y
y : Y
h : Tendsto f cofinite (𝓝 y)
⊢ Tendsto (⇑{ toFun := f, continuous_toFun := ⋯ }) (coclosedCompact X) (𝓝 y)

Tactic:
simpa [cocompact_eq_cofinite]

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
hU : IsCompact U
hV : IsCompact V
this : IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
apply this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop)

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 := ⋯
V : Set X := ⋯
hU : IsCompact U
hV : IsCompact V
this : IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ (fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K ⊆ (fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: case neg
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E)ᶜ
y : F
h : y ∉ E
⊢ y ∈ (convexHull ℝ) (↑E)ᶜ

Tactic:
exact subset_convexHull ℝ (Eᶜ : Set F) h

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
xy : x ≤ y
⊢ False

pp: case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
yx : y ≤ x
⊢ False

Tactic:
· exact hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)

Goal state after:
case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
yx : y ≤ x
⊢ False
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : eVariationOn f s = 0
x : ℝ
x✝¹ : x ∈ s
y : ℝ
x✝ : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = 0

Tactic:
simpa [h] using eVariationOn.mono (s := s) f inter_subset_left

Goal state after:
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
l : List R
h : l.SortedLE
i j k : ℕ
⊢ ∀ (hij : i < j) (hjk : j < k) (hk : k < l.length), Wbtw R l[i] l[j] l[k]

Tactic:
hij

Goal state after:
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
l : List R
h : l.SortedLE
i j k : ℕ
hij : i < j
⊢ ∀ (hjk : j < k) (hk : k < l.length), Wbtw R l[i] l[j] l[k]
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : V
p : P
⊢ z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y

Tactic:
← affineSegment_vadd_const_image,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : V
p : P
⊢ z +ᵥ p ∈ (fun x ↦ x +ᵥ p) '' affineSegment R x y ↔ z ∈ affineSegment R x y
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y z : V
⊢ Wbtw R (-x) (-y) (-z) ↔ Wbtw R x y z

Tactic:
by
  simp only [← zero_sub, wbtw_const_sub_iff]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: case inl
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : IsEmpty J
⊢ (partialSections F H).Nonempty

pp: case inr
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
⊢ (partialSections F H).Nonempty

Tactic:
· exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩

Goal state after:
case inr
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
⊢ (partialSections F H).Nonempty