mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.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
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))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
⊢ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_
    have hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖ := by
      simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x
    rcases le_total (f x) (-‖f‖ / 3) with hle₁ | hle₁
    · calc
        |g (e x) - f x| = -‖f‖ / 3 - f x := by
          rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
            abs_of_nonneg (sub_nonneg.2 hle₁)]
        _ ≤ 2 / 3 * ‖f‖ := by linarith
    · rcases le_total (f x) (‖f‖ / 3) with hle₂ | hle₂
      · simp only [neg_div] at *
        calc
          dist (g (e x)) (f x) ≤ |g (e x)| + |f x| := dist_le_norm_add_norm _ _
          _ ≤ ‖f‖ / 3 + ‖f‖ / 3 := (add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))
          _ = 2 / 3 * ‖f‖ := by linarith
      · calc
          |g (e x) - f x| = f x - ‖f‖ / 3 := by
            rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
              abs_of_nonneg (sub_nonneg.2 hle₂)]
          _ ≤ 2 / 3 * ‖f‖ := by linarith

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

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) (num g z / denom g z)).im =
    |↑(GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)

Tactic:
rw [abs_of_pos h]

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) (num g z / denom g z)).im =
    ↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I = (σ g) ↑I * denom g ↑I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0

Tactic:
σ,

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I =
      (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑I * denom g ↑I ↔
    ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑(GeneralLinearGroup.det g) < 0
⊢ num g ↑I = (σ g) ↑I * denom g ↑I ↔ ↑g 0 0 = -↑g 1 1 ∧ ↑g 0 1 = ↑g 1 0

Tactic:
σ,

Goal state after:
g : GL (Fin 2) ℝ
hg : ↑(GeneralLinearGroup.det g) < 0
⊢ num g ↑I =
      (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑I * denom g ↑I ↔
    ↑g 0 0 = -↑g 1 1 ∧ ↑g 0 1 = ↑g 1 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ (σ g) (num g ↑z / denom g ↑z) = num g ↑z / denom g ↑z

Tactic:
σ,

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) (num g ↑z / denom g ↑z) =
    num g ↑z / denom g ↑z
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ (g • z).re = (num g ↑z / denom g ↑z).re

Tactic:
change (smulAux' g z).re = _

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (smulAux' g ↑z).re = (num g ↑z / denom g ↑z).re
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℍ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z) =
    |↑(GeneralLinearGroup.det g)| * (↑z).im / Complex.normSq (denom g ↑z)

Tactic:
rw [abs_of_pos h]

Goal state after:
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
⊢ |(↑(↑N * -n) +ᵥ z).re| ≤ ↑N

Tactic:
rw [h, add_comm]

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
⊢ |z.re + ↑(-↑N * ⌊z.re / ↑N⌋)| ≤ ↑N
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : SL(2, ℝ)
hc : ↑g 1 0 ≠ 0
⊢ ∃ u v w, (fun x ↦ g • x) = (fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x

Tactic:
have h_denom (z : ℍ) := denom_ne_zero g z
  induction g using Matrix.SpecialLinearGroup.fin_two_induction with | _ a b c d h => ?_
  replace hc : c ≠ 0 := by simpa using! hc
  refine ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, ?_⟩
  ext1 ⟨z, hz⟩; ext1
  suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹ by
    simpa [modular_S_smul, coe_specialLinearGroup_apply]
  replace hc : (c : ℂ) ≠ 0 := by norm_cast
  replace h_denom : ↑c * z + d ≠ 0 := by simpa using! h_denom ⟨z, hz⟩
  replace h : (a * d - b * c : ℂ) = (1 : ℂ) := by norm_cast
  grind

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:

Tactic:
g y + dg y ≤ c + (c - a) := add_le_add hc (dgmem _).2
        _ = b := by rw [hsub, add_sub_cancel]

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

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

Tactic:
abs_of_pos b.im_pos,

Goal state after:
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * (2 * b.im))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ ↑(Ultrafilter.map g F) ≤ 𝓝 (g x)

Tactic:
F.coe_map

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ map g ↑F ≤ 𝓝 (g 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✝ : T2Space X
⊢ ProperSMul G X ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
rw [properSMul_iff_continuousSMul_ultrafilter_tendsto]

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✝ : T2Space X
⊢ (ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
x : OnePoint X
⊢ x ∈ (range some)ᶜ ↔ x = ∞

Tactic:
compl_range_coe,

Goal state after:
X : Type u_1
x : OnePoint X
⊢ x ∈ {∞} ↔ x = ∞
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X✝ : J
⊢ ∀ ⦃Y : J⦄ (f : X✝ ⟶ Y),
    ((Functor.const J).obj
              { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial }).map
          f ≫
        InducedCategory.homMk ((TopCat.limitCone FF).π.app Y) =
      InducedCategory.homMk ((TopCat.limitCone FF).π.app X✝) ≫ F.map f

Tactic:
_

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X✝ Y✝ : J
⊢ ∀ (f : X✝ ⟶ Y✝),
    ((Functor.const J).obj
              { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial }).map
          f ≫
        InducedCategory.homMk ((TopCat.limitCone FF).π.app Y✝) =
      InducedCategory.homMk ((TopCat.limitCone FF).π.app X✝) ≫ F.map f
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
⊢ UCompactlyGeneratedSpace X

Tactic:
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦
    SequentialSpace.isClosed_of_seq _ fun u p hu hup ↦ ?_

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)
⊢ p ∈ s
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: 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) ℝ)
⊢ IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}

Tactic:
convert! ProperSpace.isCompact_closedBall (0 : Matrix (Fin 2) (Fin 2) ℝ) (max √A √A')

Goal state after:
case e'_3
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) ℝ)
⊢ {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'} = Metric.closedBall 0 (max √A √A')
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₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤

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

Goal state after:
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 : ℝ
hb : b ∈ Ioi 0
⊢ a ≤ b → logCounting D a ≤ logCounting D b

Tactic:
_

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 : ℝ
hb : b ∈ Ioi 0
a✝ : a ≤ b
⊢ logCounting D a ≤ logCounting D b
Module: Mathlib.Analysis.Convex.AmpleSet

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

Tactic:
_

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

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
← h.2 xs ys,

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

Goal state before:
pp: F : Type u_1
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ F
inst✝³ : TopologicalSpace F
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set E
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
x : E
hx : x ∈ s
⊢ ⇑L '' (convexHull ℝ) (connectedComponentIn s x) = univ

Tactic:
rw [h x hx, image_univ, L.surjective.range_eq]

Goal state after:
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
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
rw [this, hfs zs ys zy]

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

Goal state before:
pp: case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
⊢ ¬a = 0 → ¬z = 0 → ¬a * ‖z‖⁻¹ = 1 → ¬a * ‖z‖⁻¹ = -1 → ¬((toClosedBall b) D) z = 0

Tactic:
_

Goal state after:
case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
a✝ : ¬a = 0
⊢ ¬z = 0 → ¬a * ‖z‖⁻¹ = 1 → ¬a * ‖z‖⁻¹ = -1 → ¬((toClosedBall b) D) z = 0
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
a✝ : ¬a = 0
⊢ ¬z = 0 → ¬a * ‖z‖⁻¹ = 1 → ¬a * ‖z‖⁻¹ = -1 → ¬((toClosedBall b) D) z = 0

Tactic:
_

Goal state after:
case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
a✝¹ : ¬a = 0
a✝ : ¬z = 0
⊢ ¬a * ‖z‖⁻¹ = 1 → ¬a * ‖z‖⁻¹ = -1 → ¬((toClosedBall b) D) z = 0
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
a✝¹ : ¬a = 0
a✝ : ¬z = 0
⊢ ¬a * ‖z‖⁻¹ = 1 → ¬a * ‖z‖⁻¹ = -1 → ¬((toClosedBall b) D) z = 0

Tactic:
_

Goal state after:
case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
a✝² : ¬a = 0
a✝¹ : ¬z = 0
a✝ : ¬a * ‖z‖⁻¹ = 1
⊢ ¬a * ‖z‖⁻¹ = -1 → ¬((toClosedBall b) D) z = 0
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
a✝² : ¬a = 0
a✝¹ : ¬z = 0
a✝ : ¬a * ‖z‖⁻¹ = 1
⊢ ¬a * ‖z‖⁻¹ = -1 → ¬((toClosedBall b) D) z = 0

Tactic:
_

Goal state after:
case h₁.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
h₁ : ¬((toClosedBall a) D) z = 0
a✝³ : ¬a = 0
a✝² : ¬z = 0
a✝¹ : ¬a * ‖z‖⁻¹ = 1
a✝ : ¬a * ‖z‖⁻¹ = -1
⊢ ¬((toClosedBall b) D) z = 0
Module: Mathlib.Analysis.Convex.BetweenList

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
inst✝ : IsOrderedRing R
p₁ p₂ p₃ : P
⊢ Wbtw R p₁ p₂ p₃ ∧ (¬p₁ = p₂ ∧ ¬p₁ = p₃) ∧ ¬p₂ = p₃ ↔ Sbtw R p₁ p₂ p₃

Tactic:
exact ⟨fun ⟨hw, ⟨h₁₂, h₁₃⟩, h₂₃⟩ ↦ ⟨hw, Ne.symm h₁₂, h₂₃⟩,
         fun h ↦ ⟨h.1, ⟨h.2.1.symm, h.left_ne_right⟩, h.2.2⟩⟩

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr
α : 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
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
⊢ eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (variationOnFromTo f s b c)

Tactic:
variationOnFromTo.eq_of_le _ _ bc,

Goal state after:
case inr
α : 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
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
⊢ eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (eVariationOn f (s ∩ Icc b c)).toReal
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s)ᶜ
⊢ ⟨x, ⋯⟩ ∉ s'

Tactic:
_

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s)ᶜ
a✝ : ⟨x, ⋯⟩ ∈ s'
⊢ False
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
have := Classical.decEq ι
  -- Restrict to `s`
  rw [Nat.add_one] at hn
  have card_ι'_le : Fintype.card s ≤ n := by
    apply Nat.le_of_lt_succ
    calc
      Fintype.card s = #s := Fintype.card_coe _
      _ < Fintype.card ι := (card_lt_iff_ne_univ _).mpr hns
      _ = n.succ := hn
  let t' : s → Finset α := fun x' => t x'
  rcases ih t' card_ι'_le (hall_cond_of_restrict ht) with ⟨f', hf', hsf'⟩
  -- Restrict to `sᶜ` in the domain and `(s.biUnion t)ᶜ` in the codomain.
  set ι'' := (s : Set ι)ᶜ
  let t'' : ι'' → Finset α := fun a'' => t a'' \ s.biUnion t
  have card_ι''_le : Fintype.card ι'' ≤ n := by
    simp_rw [ι'', ← Nat.lt_succ_iff, ← hn, ← Finset.coe_compl, coe_sort_coe]
    rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]
  rcases ih t'' card_ι''_le (hall_cond_of_compl hus ht) with ⟨f'', hf'', hsf''⟩
  -- Put them together
  have f''_notMem_biUnion : ∀ (x'') (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t := by
    intro x'' hx''
    have h := hsf'' ⟨x'', hx''⟩
    rw [mem_sdiff] at h
    exact h.2
  have im_disj :
      ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩ := by
    grind
  refine ⟨fun x => if h : x ∈ s then f' ⟨x, h⟩ else f'' ⟨x, h⟩, ?_, ?_⟩
  · refine hf'.dite _ hf'' (@fun x x' => im_disj x x' _ _)
  · intro x
    simp only
    split_ifs with h
    · exact hsf' ⟨x, h⟩
    · exact sdiff_subset (hsf'' ⟨x, h⟩)

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

Goal state before:
pp: α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
⊢ ∀ [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
_

Goal state after:
α : Type v
inst✝² : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝¹ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst✝ : Fintype ι'
⊢ ∀ (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝² : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝¹ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst✝ : Fintype ι'
⊢ ∀ (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
_

Goal state after:
α : Type v
inst✝² : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝¹ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst✝ : Fintype ι'
t'✝ : ι' → Finset α
⊢ Fintype.card ι' ≤ n →
    (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t'✝)) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t'✝ x
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
⊢ f ∈ ↑H → IsClosed {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
_

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ IsClosed {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}