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

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
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

Tactic:
trans fderiv ℝ f y (x.re • (1 : ℂ) + x.im • (I : ℂ))

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 ℝ (⇑reCLM) (F y) ∘SL fderiv ℝ F y) x = (fderiv ℝ f y) (x.re • 1 + x.im • I)

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.Harmonic.MeanValue

Goal state before:
pp: F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
⊢ Complex.reCLM (F c) = g (f c)

Tactic:
apply h₂F

Goal state after:
F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
⊢ c ∈ ball c (e + |R|)
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ reCLM (F w) = f w

Tactic:
apply h₂F

Goal state after:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ w ∈ ball c (e + R)
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: ⊢ {z | 0 < z.im} ⊆ ℂ_ℤ

Tactic:
exact fun z hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩

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

Goal state before:
pp: ⊢ {z | 0 < z.im} ∩ ℂ_ℤ = {z | 0 < z.im}

Tactic:
apply Set.inter_eq_self_of_subset_left
  exact fun z hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩

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

Goal state before:
pp: case hs
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ∀ r ∈ Set.Ioc ‖w - c‖ R, 0 ≤ r

Tactic:
· grind [norm_nonneg (w - c)]

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

Goal state before:
pp: ⊢ Continuous fun x ↦ x * log x

Tactic:
continuous_iff_continuousAt

Goal state after:
⊢ ∀ (x : ℝ), ContinuousAt (fun x ↦ x * log x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: ⊢ Continuous log⁺

Tactic:
continuous_iff_continuousAt

Goal state after:
⊢ ∀ (x : ℝ), ContinuousAt log⁺ x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, |x - a| ^ n = ∫ (x : ℝ) in 0..b - a, x ^ n

Tactic:
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
        refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl
        rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
        exact hx.1

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

Goal state before:
pp: r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) =
    (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I

Tactic:
mul_comm _ Complex.I

Goal state after:
r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (Complex.I * ↑t) =
    (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
rw [sin_sq_add_cos_sq]
      norm_num

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

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = circleAverage (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) 0 1

Tactic:
circleAverage_eq_circleAverage_zero_one

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun z ↦ log ‖↑R * z + c - a‖) 0 1 = circleAverage (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) 0 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
z : ℂ
hz : ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0
⊢ log (‖↑R‖ * ‖z + ↑R⁻¹ * (c - a)‖) = log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖

Tactic:
log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
z : ℂ
hz : ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0
⊢ log ‖↑R‖ + log ‖z + ↑R⁻¹ * (c - a)‖ = log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
⊢ Continuous fun θ ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)

Tactic:
continuous_iff_continuousAt

Goal state after:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
⊢ ∀ (x : ℝ), ContinuousAt (fun θ ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)) x
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
n : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
h_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
⊢ volume {θ | ‖circleMap 0 R θ - ρ‖ = 0} = 0

Tactic:
simpa [sub_eq_zero] using!
      (countable_singleton ρ).preimage_circleMap 0 (hR.ne') |>.measure_zero _

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

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * cos x ^ (2 * n + 1) = ∫ (x : ℝ) in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x

Tactic:
by
      simp only [_root_.pow_zero, _root_.pow_succ, mul_assoc, pow_mul, one_mul]
      congr! 5
      rw [← sq, ← sq, cos_sq']

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

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

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

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:
· exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)

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

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‖⁻¹)
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
g₁ g₂ : GL n R
⊢ mk g₁ = mk g₂ ↔ ∃ u, g₁ * (GeneralLinearGroup.scalar n) u = g₂

Tactic:
by
  simp [mk_eq_mk_iff', Matrix.GeneralLinearGroup.center_eq_range_scalar]

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

Goal state before:
pp: ⊢ ContractibleSpace ℍ

Tactic:
isEmbedding_coe.toHomeomorph.trans (.setCongr range_coe) |>.contractibleSpace_iff

Goal state after:
⊢ ContractibleSpace ↑upperHalfPlaneSet
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
hnn : 0 < ↑N
h2 : z.re + -(↑N * ↑n) = z.re - ↑n * ↑N
⊢ |z.re + -(↑N * ↑⌊z.re / ↑N⌋)| ≤ ↑N

Tactic:
h2,

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
hnn : 0 < ↑N
h2 : z.re + -(↑N * ↑n) = z.re - ↑n * ↑N
⊢ |z.re - ↑n * ↑N| ≤ ↑N
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 →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖f‖ ≤ ‖atTop.limUnder g‖

Tactic:
rw [← hge]

Goal state after:
case 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
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖(atTop.limUnder g).compContinuous e‖ ≤ ‖atTop.limUnder g‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case refine_2
z✝ w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 ↑z)

Tactic:
refine (nhds_basis_ball.le_basis_iff (nhds_basis_ball.comap _)).2 fun R hR => ?_

Goal state after:
case refine_2
z✝ w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
⊢ ∃ i, 0 < i ∧ ball z i ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z) R
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective] at hf
  exact (forget (CompHausLike P)).epi_of_epi_map hf

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed[instTopologicalSpace] {∞}

Tactic:
← compl_range_coe,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed[instTopologicalSpace] (range some)ᶜ
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[coinduced
        (fun x ↦
          match x with
          | ⟨⟨fst, i⟩, s⟩ => i s)
        inferInstance]
    s

Tactic:
isClosed_coinduced,

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed
    ((fun x ↦
        match x with
        | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
      s)
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)
⊢ IsCompact univ

Tactic:
by
    have : Tendsto ((↑) : X → OnePoint X) (cocompact X) (𝓝 ∞) := by
      rw [nhds_infty_eq]
      exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
    rw [← insert_none_range_some X]
    exact this.isCompact_insert_range_of_cocompact continuous_coe

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

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) 0 ≤ᶠ[atTop] characteristic f₁ 0 + characteristic f₂ 0

Tactic:
filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

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

Goal state before:
pp: case «1»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨1, ⋯⟩) j| ≤ √A'

Tactic:
exact Real.le_sqrt_of_sq_le <| le_trans (by fin_cases j <;> simp [sq_nonneg]) (hA' g hg)

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

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ((toClosedBall b) D).support
⊢ ∑ᶠ (z : E), ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) ≤ ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)

Tactic:
have hs : s.Finite := (toClosedBall b D).finiteSupport (isCompact_closedBall 0 |b|)

Goal state after:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ ∑ᶠ (z : E), ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) ≤ ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
have : (s ∪ t) ∩ Icc z y = s ∩ Icc z y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨ws, zw, wy⟩
        · exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩
      · rintro ⟨ws, zwy⟩; exact ⟨Or.inl ws, zwy⟩
    rw [this, hfs zs ys zy]

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

Goal state before:
pp: f : ℂ → ℂ
⊢ locallyFinsuppWithin.logCounting (divisor f univ) = logCounting f 0 - logCounting f ⊤

Tactic:
by
  simp [logCounting, ← locallyFinsuppWithin.logCounting.map_sub]

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
⊢ #s' < #(s'.biUnion fun x_1 ↦ t ↑x_1)

Tactic:
convert! ha he fun h => by simpa [← h] using mem_univ x using 2

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
⊢ (s'.biUnion fun x_1 ↦ t ↑x_1) = (image (fun z ↦ ↑z) s').biUnion t
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
x✝ : List.Wbtw R l ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑f) l)
hl : List.Wbtw R l
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑f) l)
⊢ ∀ (a b : P), f a ≠ f b → a ≠ b

Tactic:
simp [hf.ne_iff]

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

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
x✝ : List.Wbtw R l ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
hl : List.Wbtw R l
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
⊢ ∀ (a b : P), a ≠ b → f a ≠ f b

Tactic:
simp [hf.ne_iff]

Goal state after:
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 : P
v : V
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
    (AddAction.injective v).ne_iff]

Goal state after:
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
⊢ Sbtw R (-x) (-y) (-z) ↔ Sbtw R x y z

Tactic:
simp only [← zero_sub, sbtw_const_sub_iff]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
⊢ (∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l) ↔ List.Wbtw R l

Tactic:
refine ⟨fun ⟨p₁, p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
  · subst hl'l
    exact Wbtw.map hl's.wbtw _
  · by_cases hl : l = []
    · exact ⟨AddTorsor.nonempty.some, AddTorsor.nonempty.some, [], by
        simp [hl, sortedLE_iff_pairwise]⟩
    · exact ⟨l.head hl, l.getLast hl, (exists_map_eq_of_sorted_nonempty_iff_wbtw hl).2 h⟩

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case inl.w
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := ⋯
down : J' ⥤ J := ⋯
F' : J' ⥤ Type (max u v w) := ⋯
this✝ : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : IsEmpty J
⊢ (j : J) → F.obj j

Tactic:
apply isEmptyElim

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case inl.h
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := ⋯
down : J' ⥤ J := ⋯
F' : J' ⥤ Type (max u v w) := ⋯
this✝ : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : IsEmpty J
⊢ isEmptyElim ∈ F.sections

Tactic:
apply isEmptyElim

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
⊢ Convex R ↑(colStochastic R n)

Tactic:
intro x hx y hy a b ha hb h
  simp only [SetLike.mem_coe, mem_colStochastic_iff_sum] at hx hy ⊢
  simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ (↑(minCardFinsetOfMemConvexHull hx)).Nonempty

Tactic:
← @convexHull_nonempty_iff 𝕜

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ((convexHull 𝕜) ↑(minCardFinsetOfMemConvexHull hx)).Nonempty