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

Goal state before:
pp: case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e
⊢ ∃ x, x.re = u ∧ f x = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h

Goal state after:
case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = 1
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ ∃ x, x.re = u ∧ f x = e
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = u ∧ f x = e
⊢ ∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h

Goal state after:
case mpr
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
⊢ ∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
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
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ - f₂) =ᶠ[𝓝 x] 0

Tactic:
· filter_upwards [h₁.1.laplacian_sub_nhds h₂.1, h₁.2, h₂.2]
    simp_all

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F →L[ℝ] G
h : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
⊢ Δ[s] ⇑l ∘ f =ᶠ[𝓝[s] x] ⇑l ∘ Δ[s] f

Tactic:
by
  filter_upwards [(h.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
    eventually_mem_nhdsWithin] with a h₁a using h₁a.laplacianWithin_CLM_comp_left hs

Goal state after:
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
a : ℂ
⊢ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) a = a.re • (fderiv ℝ f y) 1 + a.im • (fderiv ℝ f y) I

Tactic:
simp [HasDerivAt.deriv (hF.2 y hy), g]

Goal state after:
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
| (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) = a

Tactic:
left; arg 2; arg 1
    intro θ
    rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]

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

Goal state before:
pp: w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)

Tactic:
by_cases h₁w : ‖w - c‖ = 0

Goal state after:
case pos
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ‖w - c‖ = 0
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)

case neg
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ¬‖w - c‖ = 0
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

Tactic:
by_cases h₁w : ‖w - c‖ = 0

Goal state after:
case pos
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ‖w - c‖ = 0
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

case neg
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ¬‖w - c‖ = 0
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hint
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ IntervalIntegrable (fun y ↦ ↑y * (1 + ↑y ^ 2) ^ t) MeasureTheory.volume a b

Tactic:
· apply Continuous.intervalIntegrable
    refine continuous_ofReal.mul ?_
    apply Continuous.cpow (by fun_prop) continuous_const
    intro a
    norm_cast
    exact ofReal_mem_slitPlane.2 <| add_pos_of_pos_of_nonneg one_pos <| sq_nonneg a

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

Goal state before:
pp: n : ℕ
⊢ 0 < ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
rcases even_or_odd' n with ⟨k, rfl | rfl⟩ <;>
  simp only [integral_sin_pow_even, integral_sin_pow_odd] <;>
  refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_)

Goal state after:
case inl.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 1

case inl.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 2

case inr.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 2

case inr.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 3
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₀ + ↑c * I

Tactic:
obtain ⟨cc, hcc⟩ := eq_const_of_re_eq_const h₁f h₂f h₁U h₂U

Goal state after:
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
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∃ c, ∀ x ∈ U, f x = ↑c₀ + ↑c * I
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case h
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})
y : ℝ
q : ℂ
hq : q ∈ S
⊢ q ∉ {0} → (norm ∘ cuspFunction h f) q = y → y ≤ c

Tactic:
hq2

Goal state after:
case h
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})
y : ℝ
q : ℂ
hq : q ∈ S
hq2 : q ∉ {0}
⊢ (norm ∘ cuspFunction h f) q = y → y ≤ c
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
x✝ : ℝ
⊢ cos x✝ * sin x✝ = sin (2 * x✝) / 2

Tactic:
rw [sin_two_mul]

Goal state after:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
x✝ : ℝ
⊢ cos x✝ * sin x✝ = 2 * sin x✝ * cos x✝ / 2
Module: Mathlib.Analysis.Complex.SummableUniformlyOn

Goal state before:
pp: case refine_2
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
hc : DifferentiableOn ℂ g s
⊢ DifferentiableOn ℂ (fun z ↦ ∑' (n : ι), f n z) s

Tactic:
apply hc.congr

Goal state after:
case refine_2
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
hc : DifferentiableOn ℂ g s
⊢ ∀ x ∈ s, ∑' (n : ι), f n x = g x
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
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))
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
have hc₂ : IsClosed (e '' f ⁻¹' Ici (‖f‖ / 3)) :=
    he.isClosedMap _ (isClosed_Ici.preimage f.continuous)

Goal state after:
case 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))
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case refine_3
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]

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

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
⊢ num (g * h) ((σ g) ((σ h) ↑z)) / denom (g * h) ((σ g) ((σ h) ↑z)) =
    num g (num h ((σ g) ((σ h) ↑z)) / denom h ((σ g) ((σ h) ↑z))) /
      denom g (num h ((σ g) ((σ h) ↑z)) / denom h ((σ g) ((σ h) ↑z)))

Tactic:
generalize hu : σ g (σ h z) = u

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu : (σ g) ((σ h) ↑z) = u
⊢ num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ eval 0 (f.polyToMatrix (cornerAddX M k).det).det = (f M.det).det

Tactic:
rw [← coe_evalRingHom, RingHom.map_det, ← RingHom.comp_apply,
    evalRingHom_mapMatrix_comp_polyToMatrix, f.comp_apply, RingHom.map_det]

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (f ((evalRingHom 0).mapMatrix (cornerAddX M k)).det).det = (f M.det).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z

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

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
induction l : Fintype.card m generalizing R S m with
  | zero =>
    rw [Fintype.card_eq_zero_iff] at l
    simp_rw [Matrix.det_isEmpty, map_one, det_one]
  | succ l ih =>
    have ⟨k⟩ := Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ l)
    let f' := f.polyToMatrix
    let M' := cornerAddX M k
    have : (f' M'.det).det = ((M'.map f').comp m m n n R[X]).det := by
      refine sub_eq_zero.mp <| mem_nonZeroDivisors_iff_right.mp
        (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by
          grind [Fintype.card_subtype_compl, Fintype.card_unique])
      rw [polyToMatrix_cornerAddX, ← charpoly]
      exact (Matrix.charpoly_monic _).mem_nonZeroDivisors
    rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]

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
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ Icc (h x) (h y)
⊢ ↑z ∈ t'

Tactic:
rw [← h.image_Icc] at hz

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
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ ⇑h '' Icc x y
⊢ ↑z ∈ t'
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ (√(1 + x ^ 2) + x) * (√(1 + x ^ 2) - x) = 1

Tactic:
← sq_sub_sq,

Goal state after:
x : ℝ
⊢ √(1 + x ^ 2) ^ 2 - x ^ 2 = 1
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ (2 ^ 2 * (z.im * w.im) + dist ↑z ↑w ^ 2) / (2 ^ 2 * (z.im * w.im)) =
    dist (↑z) ((starRingEnd ℂ) ↑w) ^ 2 / (2 ^ 2 * (z.im * w.im))

pp: z w : ℍ
⊢ 0 ≤ z.im * w.im

pp: z w : ℍ
⊢ (2 * √(z.im * w.im)) ^ 2 ≠ 0

pp: case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

pp: case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Tactic:
· congr 1
    simp only [Complex.dist_eq, Complex.sq_norm, Complex.normSq_sub, Complex.normSq_conj,
      Complex.conj_conj, Complex.mul_re, Complex.conj_re, Complex.conj_im, coe_im]
    ring

Goal state after:
z w : ℍ
⊢ 0 ≤ z.im * w.im

z w : ℍ
⊢ (2 * √(z.im * w.im)) ^ 2 ≠ 0

case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' t)
this : IsOpen[inst✝] (some ⁻¹' ⋃₀ S)
s : Set (OnePoint X)
hsS : s ∈ S
hs : ∞ ∈ s
⊢ (some ⁻¹' ⋃₀ S)ᶜ ⊆ (some ⁻¹' s)ᶜ

Tactic:
exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)

Goal state after:
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
⊢ Tendsto OnePoint.some atTop (𝓝 ∞)

Tactic:
← Nat.cofinite_eq_atTop,

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
⊢ Tendsto OnePoint.some cofinite (𝓝 ∞)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R

Tactic:
· simp_rw [← norm_inv]
    apply h₁f.inv.meromorphicOn.circleIntegrable_posLog_norm

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r =
    ∑ c ∈ s, circleAverage (fun x ↦ log⁺ ‖f c x‖) 0 r + log ↑s.card

Tactic:
nth_rw 2 [← circleAverage_const (log s.card) 0 r]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r =
    ∑ c ∈ s, circleAverage (fun x ↦ log⁺ ‖f c x‖) 0 r + circleAverage (fun x ↦ log ↑s.card) 0 r
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ characteristic (f₁ + f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun x ↦ log 2

Tactic:
by
  filter_upwards [Filter.eventually_ge_atTop 1] with r hr
    using characteristic_add_top_le h₁f₁ h₁f₂ hr

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log⁺ ‖f x‖) 0 R + logCounting f ⊤ R =
    circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) 0 1

Tactic:
← proximity_top,

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ proximity f ⊤ R + logCounting f ⊤ R =
    circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) 0 1
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ StrictMonoOn (logCounting (single e 1)) (Ioi ‖e‖)

pp: case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ MonotoneOn (logCounting (D - single e 1)) (Ioi ‖e‖)

Tactic:
· intro a ha b hb hab
    rw [mem_Ioi] at ha hb
    rw [logCounting_single_eq_log_sub_const ha.le, logCounting_single_eq_log_sub_const hb.le]
    gcongr
    exact (norm_nonneg e).trans_lt ha

Goal state after:
case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ MonotoneOn (logCounting (D - single e 1)) (Ioi ‖e‖)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
r : ℝ
hr : R₀ ≤ r
⊢ logCounting D' r = ∑ c ∈ t, logCounting (single c 1) r

Tactic:
simp [hD']

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ locallyFinsuppWithin.logCounting (divisor (fun x ↦ (f₁ * f₂) x) univ)⁺ r ≤
    (locallyFinsuppWithin.logCounting (divisor (fun x ↦ f₁ x) univ)⁺ +
        locallyFinsuppWithin.logCounting (divisor (fun x ↦ f₂ x) univ)⁺)
      r

Tactic:
divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ locallyFinsuppWithin.logCounting (divisor f₁ univ + divisor f₂ univ)⁺ r ≤
    (locallyFinsuppWithin.logCounting (divisor (fun x ↦ f₁ x) univ)⁺ +
        locallyFinsuppWithin.logCounting (divisor (fun x ↦ f₂ x) univ)⁺)
      r
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ locallyFinsuppWithin.logCounting (divisor (f₁ * f₂) univ)⁻ r ≤
    (locallyFinsuppWithin.logCounting (divisor f₁ univ)⁻ + locallyFinsuppWithin.logCounting (divisor f₂ univ)⁻) r

Tactic:
divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ locallyFinsuppWithin.logCounting (divisor f₁ univ + divisor f₂ univ)⁻ r ≤
    (locallyFinsuppWithin.logCounting (divisor f₁ univ)⁻ + locallyFinsuppWithin.logCounting (divisor f₂ univ)⁻) r
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
⊢ 0 ≤ φ 0

Tactic:
have := φst ▸ mapsTo_image φ (Icc 0 s)

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ 0 ≤ φ 0