mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ0' : μ s ≠ 0
c : ℝ
hc : c ∈ uIoo a b
heq : f c = ⨍ (x : ℝ) in uIoo a b, f x ∂μ
⊢ f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
by rwa [← setAverage_congr hs_ev]

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

Goal state before:
pp: ⊢ -1 + 1 = 0

Tactic:
neg_add_cancel

Goal state after:
⊢ 0 = 0
Module: Mathlib.Analysis.Complex.Poisson

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

Tactic:
by
  simp [herglotzRieszKernel_fun_def]

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

Goal state before:
pp: ⊢ Tendsto (fun x ↦ log (log x)) (nhdsWithin 0 {0}ᶜ) (cobounded ℝ)

Tactic:
have : Tendsto log atBot atTop := by
    convert tendsto_log_atTop.comp tendsto_neg_atBot_atTop; ext; simp

Goal state after:
this : Tendsto log atBot atTop
⊢ Tendsto (fun x ↦ log (log x)) (nhdsWithin 0 {0}ᶜ) (cobounded ℝ)
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ (fun x ↦ x ^ r.re) x = (fun t ↦ ‖↑t ^ r‖) x

Tactic:
rw [uIoc_of_le hc] at hx

Goal state after:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ (fun x ↦ x ^ r.re) x = (fun t ↦ ‖↑t ^ r‖) x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ ContinuousAt (fun x ↦ ↑x ^ r) x

Tactic:
rw [uIoc_of_le hc] at hx

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ ContinuousAt (fun x ↦ ↑x ^ r) x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv.refine_1
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ x ≠ 0

Tactic:
rcases le_total c 0 with (hc | hc)

Goal state after:
case hderiv.refine_1.inl
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : c ≤ 0
⊢ x ≠ 0

case hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
by
        simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]

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

Goal state before:
pp: a b : ℝ
⊢ (∫ (x : ℝ) in a..0, log x) + ∫ (x : ℝ) in 0..b, log x = b * log b - a * log a - b + a

pp: case hab
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume a 0

pp: case hbc
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b

Tactic:
· rw [intervalIntegral.integral_symm, integral_log_from_zero, integral_log_from_zero]
    ring

Goal state after:
case hab
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume a 0

case hbc
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
by
  rcases lt_trichotomy 1 ‖a‖ with h | h | h
  · rw [circleAverage_log_norm_sub_const₂ h]
    apply (posLog_eq_log _).symm
    simp_all [le_of_lt h]
  · rw [eq_comm, circleAverage_log_norm_sub_const₁ h.symm, posLog_eq_zero_iff]
    simp_all
  · rw [eq_comm, circleAverage_log_norm_sub_const₀ h, posLog_eq_zero_iff]
    simp_all [le_of_lt h]

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

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
grw [norm_add_le, ← norm_sub_norm_le]

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ (‖circleMap 0 r θ‖ + ‖w‖) / (‖circleMap 0 r θ‖ - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)

case hd
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ 0 < ‖circleMap 0 r θ‖ - ‖w‖
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero ↑n
this : NeZero n
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ ↑n, ⋯⟩

Tactic:
exact isOpenQuotientMap_pow_compl_zero n

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a = b

Tactic:
rw [← hf_inv b, hab]

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a = (fun x ↦ x ^ 2) (-f a)
Module: Mathlib.Topology.UrysohnsBounded

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a ≤ (BoundedContinuousFunction.const X a + (b - a) • f) x

Tactic:
by dsimp; nlinarith [(hf01 x).1]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im / ↑n

Tactic:
div_pos_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero <| NeZero.ne _)

Goal state after:
n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp
g : GL (Fin 2) ℝ
h : (↑g).det < 0
⊢ (∃ z, g • z = z) → (↑g).trace = 0

Tactic:
rintro ⟨z, hz⟩
    linear_combination
      (norm := { simp [σ, h.not_gt, num, denom, z.im_ne_zero, Matrix.trace_fin_two, field] })
      congr($(gl_smul_eq_iff_num_eq.mp hz).im / z.im)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.left
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ m ∉ Set.range ⇑(scalar (Fin 2))

pp: case mpr.right
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ m.discr = 0

Tactic:
· refine fun ⟨b, hb⟩ ↦ hn0 ?_
      rw [← sub_eq_iff_eq_add'] at hm
      simpa only [← hm, ← hb, ← map_sub, ← map_pow, ← map_zero (scalar (Fin 2)), scalar_inj,
        sq_eq_zero_iff] using hnsq

Goal state after:
case mpr.right
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ m.discr = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case refine_1
g : GL (Fin 2) ℝ
⊢ Continuous ⇑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else conjCAE)

Tactic:
split_ifs
      exacts [continuous_id, continuous_conj]

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

Goal state before:
pp: z : ℍ
⊢ ModularGroup.T • z = 1 +ᵥ z

Tactic:
simpa only [zpow_one, Int.cast_one] using modular_T_zpow_smul z 1

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
a : ℝ
ha : IsGLB (range ⇑f) a
hb : IsLUB (range ⇑f) a
hmem : ∀ (x : X), f x ∈ Icc a a
hle : a ≤ a
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
have : ∀ x, f x = a := by simpa using hmem
    use const Y a
    simp [this, funext_iff]

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ (norm ℝ) z = normSq z

Tactic:
by
  rw [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex,
    Matrix.det_fin_two, normSq_apply]
  simp

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

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ -(M k j * M k k) + M k j * M k k = 0

pp: case hc
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ j ∈ {x | ¬x = k}

Tactic:
neg_add_cancel

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ 0 = 0

case hc
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ j ∈ {x | ¬x = k}
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ sinh (2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im))) / 2) = dist ↑z ↑w / (2 * √(z.im * w.im))

Tactic:
mul_div_cancel_left₀ (arsinh _) two_ne_zero,

Goal state after:
z w : ℍ
⊢ sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) = dist ↑z ↑w / (2 * √(z.im * w.im))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case inl
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)

Tactic:
trans Ordering.gt

Goal state after:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ cmp (dist z w) r = Ordering.gt

z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ Ordering.gt = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X ↦ ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E.symm ⁻¹' S)

Tactic:
← E.image_eq_preimage_symm

Goal state after:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X ↦ ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E '' S)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
x : α
⊢ (stoneCechExtend hg ∘ stoneCechUnit) x = g x

Tactic:
rw [stoneCechExtend, Function.comp_apply, stoneCechUnit, T2Quotient.lift_mk]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
x : α
⊢ preStoneCechExtend hg (preStoneCechUnit x) = g x
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen[inst✝] (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen[inst✝] (some ⁻¹' t)
⊢ ∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ

Tactic:
rintro ⟨hms', hmt'⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen[inst✝] (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen[inst✝] (some ⁻¹' t)
hms' : ∞ ∈ s
hmt' : ∞ ∈ t
⊢ IsCompact (some ⁻¹' (s ∩ t))ᶜ
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
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
⊢ False

Tactic:
let g : Y ⟶ Z := ofHom _
      ⟨fun y' => ⟨⟨φ y', hφ01 y'⟩⟩,
        continuous_uliftUp.comp (φ.continuous.subtype_mk fun y' => hφ01 y')⟩

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))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
⊢ False
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 := ⋯
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

Tactic:
exact Set.preimage_mono Set.subset_fst_image_prod_snd_image

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

Goal state before:
pp: X✝ : Type u
Y : Type v
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactlyGeneratedSpace (X i)
⊢ CompactlyGeneratedSpace ((i : ι) × X i)

Tactic:
by
  refine compactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sigma_iff.2 fun i ↦
    CompactlyGeneratedSpace.isClosed' fun K _ _ _ f hf ↦ ?_
  let g : ULift.{u} K → (Σ i, X i) := Sigma.mk i ∘ f ∘ ULift.down
  have hg : Continuous g := continuous_sigmaMk.comp <| hf.comp continuous_uliftDown
  exact (h _ g hg).preimage continuous_uliftUp

Goal state after:
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:
apply h₁f.meromorphicOn.circleIntegrable_posLog_norm

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
h : Meromorphic f
R : ℝ
⊢ ‖(characteristic f ⊤ - characteristic (fun x ↦ f x - a₀) ⊤) R‖ ≤ (log⁺ ‖a₀‖ + log 2) * ‖1 R‖

Tactic:
simpa using abs_characteristic_sub_characteristic_shift_le h

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

Goal state before:
pp: case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [← circleAverage_congr_codiscreteWithin
      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm]
    simp_rw [norm_sub_rev]
    rw [circleAverage_log_norm_sub_const_eq_posLog]

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

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi 0 → a ≤ b → characteristic f ⊤ a ≤ characteristic f ⊤ b

Tactic:
b

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
⊢ b ∈ Ioi 0 → a ≤ b → characteristic f ⊤ a ≤ characteristic f ⊤ b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : a ∈ Ioi 0
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi 0 → a ≤ b → logCounting D a ≤ logCounting D b

Tactic:
b

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
⊢ b ∈ Ioi 0 → a ≤ b → logCounting D a ≤ logCounting D b
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
a : ℝ
ha : a ∈ Ioi ‖e‖
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi ‖e‖ → a < b → logCounting (single e 1) a < logCounting (single e 1) b

Tactic:
b

Goal state after:
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
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
⊢ b ∈ Ioi ‖e‖ → a < b → logCounting (single e 1) a < logCounting (single e 1) b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
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
a : ℝ
ha : a ∈ Ioi ‖e‖
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi ‖e‖ → a ≤ b → logCounting (D - single e 1) a ≤ logCounting (D - single e 1) b

Tactic:
b

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
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
⊢ b ∈ Ioi ‖e‖ → a ≤ b → logCounting (D - single e 1) a ≤ logCounting (D - single e 1) b
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
⊢ edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0

Tactic:
by
  dsimp only [naturalParameterization]
  have : Nonempty α := ⟨a⟩
  obtain ⟨cs, hc⟩ := Function.invFunOn_pos (b := variationOnFromTo f s a b) ⟨b, bs, rfl⟩
  rw [variationOnFromTo.eq_left_iff hf as cs bs] at hc
  apply variationOnFromTo.edist_zero_of_eq_zero hf cs bs hc

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

Goal state before:
pp: case cons.refine_1.refine_1.cons
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
inst✝ : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) →
    Pairwise (Wbtw R head) tail → List.Wbtw R tail → Pairwise (Sbtw R head) tail
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: head2 :: tail)
hp : Pairwise (Wbtw R head) (head2 :: tail)
ht : List.Wbtw R (head2 :: tail)
⊢ Pairwise (Sbtw R head) (head2 :: tail)

Tactic:
rw [pairwise_cons] at hp hpne hpne ⊢

Goal state after:
case cons.refine_1.refine_1.cons
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
inst✝ : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) →
    Pairwise (Wbtw R head) tail → List.Wbtw R tail → Pairwise (Sbtw R head) tail
hpne : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ (∀ a' ∈ tail, head2 ≠ a') ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail
hp : (∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail
ht : List.Wbtw R (head2 :: tail)
⊢ (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg.refine_1
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
a : R
ha : a ∈ l''
⊢ 0 ≤ r + (1 - r) * a

Tactic:
have := hl''0 a ha

Goal state after:
case neg.refine_1
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
a : R
ha : a ∈ l''
this : 0 ≤ a
⊢ 0 ≤ r + (1 - r) * a