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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε ∈ Iio 0
⊢ ‖cexp (↑ε * z) • f z‖ ≤ C

Tactic:
change ε < 0 at ε₀

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
⊢ ‖cexp (↑ε * z) • f z‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inl
a b r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re

Tactic:
rwa [Complex.ofReal_re]

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

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

Tactic:
· 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.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ ↑R * z + c - a = ↑R * (z + ↑R⁻¹ * (c - a))

Tactic:
Complex.ofReal_inv R

Goal state after:
case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ ↑R * z + c - a = ↑R * (z + (↑R)⁻¹ * (c - a))
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
let q := 𝕢 h z

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case neg.h
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
⊢ 0 < ‖z - w‖ ^ 2

Tactic:
suffices z ≠ w by simpa [sq_pos_iff, sub_eq_zero]

Goal state after:
case neg.h
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
⊢ z ≠ w
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case hF_meas
ρ 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 : ℕ) in atTop,
    AEStronglyMeasurable (fun x ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) (volume.restrict (uIoc 0 (2 * π)))

pp: case h_bound
ρ 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 : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

pp: case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

pp: case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))

Tactic:
· -- The herglotzLogIntegrand is AEStronglyMeasurable
    filter_upwards [hr_tendsto.eventually (lt_mem_nhds hw)] with n hn
    exact continuous_herglotzLogIntegrand_circle hρ (hr_lt n) hn |>.aestronglyMeasurable

Goal state after:
case h_bound
ρ 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 : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t

Tactic:
exact hx

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

Goal state before:
pp: case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * log (R * ‖c - x‖⁻¹)

Tactic:
· rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))), log_inv]
      ring

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t

Tactic:
exact hx

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ Monotone f

Tactic:
rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log R - ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log ‖c - u‖ +
      log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
rw [← finsum_sub_distrib]
      · simp_rw [← mul_sub]
      repeat apply h₃f.subset (fun _ ↦ (by simp_all))

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

Goal state before:
pp: cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : cd ≠ 0
⊢ ↑(cd 0) * z + ↑(cd 1) ≠ 0

Tactic:
by
  contrapose h
  have : cd 0 = 0 := by
    -- we will need this twice
    apply_fun Complex.im at h
    simpa only [Complex.add_im, Complex.mul_im, Complex.ofReal_im, zero_mul, add_zero,
      Complex.zero_im, mul_eq_zero, hz, or_false] using! h
  simp only [this, zero_mul, Complex.ofReal_zero, zero_add, Complex.ofReal_eq_zero] at h
  ext i
  fin_cases i <;> assumption

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

Goal state before:
pp: case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
⊢ (↑n * a ^ (n - 1)) • m ≠ 0

Tactic:
suffices a ≠ 0 by simp [this, hm0, hn]

Goal state after:
case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
⊢ a ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: ⊢ atImInfty.NeBot

Tactic:
refine comap_neBot_iff_frequently.mpr (Eventually.frequently ?_)

Goal state after:
⊢ ∀ᶠ (x : ℝ) in atTop, x ∈ Set.range im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Goal state before:
pp: s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ ∫⁻ (a : ℍ) in s, ↑((1 / NNReal.mk a.im ⋯) ^ 2) ∂Measure.comap UpperHalfPlane.coe volume =
    ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s ∩ Set.range UpperHalfPlane.coe, ↑((1 / ‖z.im‖₊) ^ 2)

Tactic:
← Measure.restrict_restrict',

Goal state after:
s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ ∫⁻ (a : ℍ) in s, ↑((1 / NNReal.mk a.im ⋯) ^ 2) ∂Measure.comap UpperHalfPlane.coe volume =
    ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s, ↑((1 / ‖z.im‖₊) ^ 2) ∂volume.restrict (Set.range UpperHalfPlane.coe)

s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ MeasurableSet (Set.range UpperHalfPlane.coe)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ dist c (inversion c R x) = R ^ 2 / dist c x

Tactic:
dist_comm c,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist c x
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist c x

Tactic:
dist_comm c,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: 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

Tactic:
rw [dist_self, zero_mul]

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
⊢ 0 ≤ dist c b * dist c d + dist b c * dist c d
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))

Tactic:
gcongr
    exact EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ))

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

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

Tactic:
have hr₀' : 0 ≤ w.im * Real.sinh r := by positivity

Goal state after:
case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
⊢ cmp (dist z w) r = 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 : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
⊢ ∀ {A B : CompHausLike P} (f : A ⟶ B) [IsIso ((forget (CompHausLike P)).map f)], IsIso f

Tactic:
intro A B f hf

Goal state after:
P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf : IsIso ((forget (CompHausLike P)).map f)
⊢ IsIso f
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := ⋯
⊢ IsClosed {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
have :
          { u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j } =
            ⋂ (i : J) (j : J) (f : i ⟶ j), { u | F.map f (u i) = u j } := by
          ext1
          simp only [Set.mem_iInter, Set.mem_ofPred_eq]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
⊢ IsClosed {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X✝ : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ t ≤ compactlyGenerated X

Tactic:
rw [DiscreteTopology.eq_bot (t := t)]

Goal state after:
X✝ : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ⊥ ≤ compactlyGenerated X
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
⊢ IsProperMap fun gx ↦ (gx.1 • ↑gx.2, gx.2)

Tactic:
have Φ_proper : IsProperMap Φ := ProperSMul.isProperMap_smul_pair

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
⊢ IsProperMap fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
⊢ UCompactlyGeneratedSpace (X ⊕ Y)

Tactic:
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sum_iff.2 ⟨?_, ?_⟩

Goal state after:
case refine_1
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tX] (Sum.inl ⁻¹' s)

case refine_2
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tY] (Sum.inr ⁻¹' s)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x ↦ ↑(f x)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧ Continuous[inst✝¹, instTopologicalSpace] fun x ↦ ↑(f x)) ↔
    Continuous[inst✝¹, instTopologicalSpace] (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)

Tactic:
exact and_comm

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

Goal state before:
pp: case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 0 ≤ logCounting (single e 1) ℓ

pp: case hab
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ logCounting (single e 1) ℓ ≤ logCounting D ℓ

Tactic:
· apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ

Goal state after:
case hab
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ logCounting (single e 1) ℓ ≤ logCounting D ℓ
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : Meromorphic f
hg : AnalyticOn 𝕜 g univ
⊢ logCounting (f + g) ⊤ = logCounting f ⊤

Tactic:
by
  simp only [logCounting, ↓reduceDIte]
  rw [hf.meromorphicOn.negPart_divisor_add_of_analyticNhdOn_right
    (isOpen_univ.analyticOn_iff_analyticOnNhd.1 hg)]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
⊢ ∃ l c, s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c ≤ s.domRestrict φ ∧ re (l x) + c = a

Tactic:
let c := (re (L (0, 1)))⁻¹

Goal state after:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
⊢ ∃ l c, s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c ≤ s.domRestrict φ ∧ re (l x) + c = a
Module: Mathlib.Analysis.Convex.Between

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

Tactic:
by
  rw [← affineSegment_vadd_const_image, (vadd_right_injective p).mem_set_image]

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:
by
  rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
    (AddAction.injective v).ne_iff]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ ≠ 0
⊢ ∃ l c,
    (∀ (i : ℕ), s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) ≤ s.domRestrict φ) ∧
      ⨆ i, s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) = s.domRestrict φ

Tactic:
obtain ⟨x, hx⟩ := Function.ne_iff.1 hsφ
      have : s = ∅ := by have := congrFun h𝓕'.2.1 x; simp_all
      grind

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      range ⇑(ConcreteCategory.hom ((F.toPreimages s).map f)) ⊆
        range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (g ≫ f)))

Tactic:
refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
⊢ range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (f₂ ≫ f₁))) ⊆
    range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁)))
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mpr
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ affineSegment R (s.points 0) (s.points 1) → p ∈ s.closedInterior

Tactic:
rintro ⟨r, ⟨h0, h1⟩, rfl⟩

Goal state after:
case mpr
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
⊢ (lineMap (s.points 0) (s.points 1)) r ∈ s.closedInterior
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ Injective fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩

Tactic:
intro i i'
        have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
        have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
        simp only
        rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
        let uii' := u (Opposite.op ({i, i'} : Finset ι))
        exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), ∃ i f, (range ⇑(ConcreteCategory.hom (F.map f))).Finite
⊢ F.IsMittagLeffler

Tactic:
intro j
  obtain ⟨i, hi, hf⟩ := h j
  obtain ⟨m, ⟨i, f, hm⟩, hmin⟩ := Finset.wellFoundedLT.wf.has_min
    { s : Finset (F.obj j) | ∃ (i : _) (f : i ⟶ j), ↑s = range (F.map f) }
    ⟨_, i, hi, hf.coe_toFinset⟩
  refine ⟨i, f, fun k g =>
    (F.ranges_directed j).directedOn_range.is_bot_of_is_min ⟨⟨i, f⟩, rfl⟩ ?_ _ ⟨⟨k, g⟩, rfl⟩⟩
  rintro _ ⟨⟨k', g'⟩, rfl⟩ hl
  refine (eq_of_le_of_not_lt hl ?_).ge
  have := hmin _ ⟨k', g', (m.finite_toSet.subset <| hm.substr hl).coe_toFinset⟩
  rwa [← Finset.coe_ssubset, Set.Finite.coe_toFinset, hm] at this

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ b₁ ∈ (single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
dsimp [single]; split_ifs <;> simp [*, eq_comm]

Goal state after: