mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
· have hgo : analyticOrderAt _ x = 1 := hg.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hg'
    rw [hf.meromorphicOrderAt_comp hg, hgo] <;>
    simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top, hgo]

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
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
⊢ Δ[s] f₁ + f₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) + Δ[s] f₂

Tactic:
nth_rw 1 [← 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
⊢ Δ[s] f₁ + f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) + Δ[s] f₂
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
⊢ Δ[s] f₁ - f₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) - Δ[s] f₂

Tactic:
nth_rw 1 [← 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
⊢ Δ[s] f₁ - f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
⊢ ∀ (z w : ℂ), f z = f w

Tactic:
intro z w

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
⊢ f z = f w
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in Ioc a b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
integral_of_le h

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in Ioc a b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in Ioc a b, f x ∂volume
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ✝ : ℂ
hζ✝ : ζ✝.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ✝).re
hz_im : 0 ≤ (cexp ζ✝).im
hzne : cexp ζ✝ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖f (cexp ↑ζ.re * (↑(Real.cos (π / 2)) + ↑(Real.sin (π / 2)) * I))‖ ≤ C

Tactic:
Real.cos_pi_div_two,

Goal state after:
case inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ✝ : ℂ
hζ✝ : ζ✝.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ✝).re
hz_im : 0 ≤ (cexp ζ✝).im
hzne : cexp ζ✝ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖f (cexp ↑ζ.re * (↑0 + ↑(Real.sin (π / 2)) * I))‖ ≤ C
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ 0 < (-↑z)⁻¹.im

Tactic:
by
  simpa [neg_div] using div_pos z.im_pos (normSq_pos z)

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

Goal state before:
pp: ⊢ (fun x ↦ deriv (fun x ↦ x * log x) x) =ᶠ[atTop] fun x ↦ log x + 1

Tactic:
EventuallyEq,

Goal state after:
⊢ ∀ᶠ (x : ℝ) in atTop, deriv (fun x ↦ x * log x) x = log x + 1
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) =ᶠ[atTop] fun x ↦ log x + 1

Tactic:
EventuallyEq,

Goal state after:
⊢ ∀ᶠ (x : ℝ) in atTop, derivWithin (fun x ↦ x * log x) (Set.Ioi x) x = log x + 1
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
⊢ ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = ∮ (z : ℂ) in C(0, R), (↑q / (↑q * z - W)) • f z

Tactic:
by
      apply circleIntegral.integral_congr hR.le fun z hz ↦ ?_
      have hz : z ≠ 0 := by aesop
      match_scalars
      field

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

Goal state before:
pp: t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ

Tactic:
apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)

Goal state after:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ cos 0 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: this : AnalyticOnNhd ℝ (fun x ↦ 4 * sin x ^ 2) Set.univ
⊢ {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:
have := this.preimage_zero_mem_codiscrete (x := π / 2)

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

Goal state before:
pp: h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝[≠] 0)

Tactic:
by
  refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_
    (.of_forall fun q ↦ exp_ne_zero _)
  rw [tendsto_zero_iff_norm_tendsto_zero]
  simp only [norm_qParam]
  apply (tendsto_comap'_iff (m := fun y ↦ Real.exp (-2 * π * y / h)) (range_im ▸ univ_mem)).mpr
  refine Real.tendsto_exp_atBot.comp (.atBot_div_const hh (tendsto_id.const_mul_atTop_of_neg ?_))
  simpa using Real.pi_pos

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}
z : E
h1 : AnalyticAt ℂ (gray z) 0
hz : z ∈ sphere 0 1
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
refine h7.trans (map_mono ?_)

Goal state after:
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}
z : E
h1 : AnalyticAt ℂ (gray z) 0
hz : z ∈ sphere 0 1
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
⊢ map (ray z) (𝓝 0) ≤ 𝓝 z₀
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: p : ℂ[X]
h : ¬∃ x, C x = p
⊢ IsOpenQuotientMap fun x ↦ eval x p

Tactic:
obtain ⟨x, eq⟩ | hp := (AnalyticOnNhd.eval_polynomial p).is_constant_or_isOpenMap

Goal state after:
case inl
p : ℂ[X]
h : ¬∃ x, C x = p
x : ℂ
eq : ∀ (z : ℂ), eval z p = x
⊢ IsOpenQuotientMap fun x ↦ eval x p

case inr
p : ℂ[X]
h : ¬∃ x, C x = p
hp : IsOpenMap fun x ↦ eval x p
⊢ IsOpenQuotientMap fun x ↦ eval x p
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

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

Tactic:
intro z hz
  rw [mem_rootSet, coe_aeval_eq_eval] at hz
  rw [eq_centerMass_of_eval_derivative_eq_zero h₀ hz.2]
  apply Finset.centerMass_mem_convexHull
  · simp [derivRootWeight_nonneg]
  · apply sum_derivRootWeight_pos h₀
  · simp [mem_rootSet]

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

Goal state before:
pp: f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ z ∈ Metric.ball c ((z - c).re + 1)

Tactic:
Metric.mem_ball,

Goal state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ dist z c < (z - c).re + 1
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel c w * fun x ↦ log ‖x - ρ‖) c R = log ‖w - ρ‖

Tactic:
by
  simp only [← circleAverage_map_add_const, Pi.mul_apply, Function.comp_apply, add_zero]
  conv =>
    left; arg 1
    intro z
    rw [(by ring : (z + 0 + c) - ρ = z - (ρ - c))]
    arg 1; arg 1
    rw [add_zero, herglotzRieszKernel_add_const c w z]
  have : (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    (Complex.re ∘ herglotzRieszKernel 0 (w - c)) • (log ‖· - (ρ - c)‖) := by rfl
  rw [this, circleAverage_re_herglotzRieszKernel_mul_log₀ (by simp_all)
    (by simp_all [mem_ball_iff_norm.1 hw])]
  simp

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ sqrt a = ↑√(re a)

Tactic:
sqrt_eq_ite,

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) a).sqrt else ↑√(re a)) = ↑√(re a)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ sqrt (-a) = I * sqrt a

Tactic:
sqrt_eq_ite,

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) (-a)).sqrt else ↑√(re (-a))) = I * sqrt a
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ IsOpenMap fun τ ↦ ‖↑τ‖

Tactic:
by
  refine .of_nhds_le fun τ U hU ↦ ?_
  obtain ⟨s, hs, hs'⟩ := Filter.mem_map_iff_exists_image.mp hU
  simp_rw [← isOpenEmbedding_coe.image_mem_nhds, Metric.mem_nhds_iff] at hs ⊢
  obtain ⟨ε, hεpos, hεs⟩ := hs
  refine ⟨ε, hεpos, subset_trans (fun r hr ↦ ?_) hs'⟩
  have hr' : 0 ≤ r := by
    by_contra! hr'
    rw [mem_ball_iff_norm, Real.norm_eq_abs, abs_lt] at hr
    have : ‖(τ : ℂ)‖ < ε := by linarith
    have : 0 ∈ Metric.ball (τ : ℂ) ε := by rwa [mem_ball_iff_norm', sub_zero]
    simpa [UpperHalfPlane.ne_zero] using hεs this
  have : r / ‖(τ : ℂ)‖ * (τ : ℂ) ∈ Metric.ball (τ : ℂ) ε := by
    rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]
  obtain ⟨ξ, hξs, hξτ⟩ := Set.mem_of_mem_of_subset this hεs
  use ξ, hξs
  simp_rw [hξτ, norm_mul, norm_div, norm_real, norm_norm]
  rw [div_mul_cancel₀ _ (by simpa using τ.ne_zero), Real.norm_of_nonneg hr']

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

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℂ
⊢ denom (J * g) τ = denom g τ

Tactic:
simp [denom, vecMul, vecHead, vecTail]

Goal state after:
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)
⊢ 0 < dg y

Tactic:
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: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
have ht_sub : t' ⊆ Ioo (-1 : ℝ) 1 := image_subset_iff.2 fun x _ => (h x).2

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
⊢ IsIntegral R ((norm K) x)

Tactic:
let F := K⟮x⟯

Goal state after:
case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ IsIntegral R ((norm K) x)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
let F := K⟮x⟯

Goal state after:
case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
rcases eq_or_ne c a with (rfl | hc)

Goal state after:
case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d

case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x ↦ sinh x - x) x

Tactic:
deriv_fun_sub,

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv sinh x - deriv (fun x ↦ x) x

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
gx : G × X
hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)
hgx2 : ↑𝒰 ≤ 𝓝 gx
⊢ gx.1 • x₂ = x₁

Tactic:
simp only [Prod.mk.injEq] at hgx1

Goal state after:
case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
gx : G × X
hgx2 : ↑𝒰 ≤ 𝓝 gx
hgx1 : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
⊢ gx.1 • x₂ = x₁
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous[_, t] (f ∘ ⇑g)
⊢ Continuous[compactlyGenerated X, t] f

Tactic:
rw [continuous_coinduced_dom]
  continuity

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
⊢ False

Tactic:
have : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | 0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst✝¹] s
⊢ CompactlyGeneratedSpace X

Tactic:
refine compactlyGeneratedSpace_of_isOpen fun s hs ↦ h s fun K hK ↦ ?_

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst✝¹] s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst✝¹] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | ¬0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ)

Tactic:
rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]

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 ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ (eVariationOn f (s ∩ Icc x y)).toReal = ↑l * (y - x)

Tactic:
h xs ys xy

Goal state after:
case mp.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ (ENNReal.ofReal (↑l * (y - x))).toReal = ↑l * (y - x)
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
a✝ : x ∈ univ
⊢ (convexHull ℝ) (connectedComponent x) = univ

Tactic:
PreconnectedSpace.connectedComponent_eq_univ,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
a✝ : x ∈ univ
⊢ (convexHull ℝ) univ = univ
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
A : E → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), {x | s x < d} = ⋃ f ∈ A d, U f d
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
⊢ ∃ f ∈ A d, f x < d

Tactic:
have : x ∈ {y | s y < d} := hd.1
    simpa only [hA d, mem_iUnion₂, exists_prop, U, mem_ofPred_eq] using this

Goal state after: