mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
i : ℕ
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
this : some x = some y
⊢ x = y

Tactic:
by injection this

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = some y

Tactic:
← hy

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = xs[j]?
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
hB_inj : Function.Injective ⇑B
⊢ IsEmbedding fun x1 x2 ↦ (B x1) x2

Tactic:
convert! (LinearMap.coe_injective.comp hB_inj |>.isEmbedding_induced)

Goal state after:
case e'_3
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
hB_inj : Function.Injective ⇑B
⊢ inst = TopologicalSpace.induced (DFunLike.coe ∘ ⇑B) Pi.topologicalSpace
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D : Set X✝
inst✝¹ : RelCWComplex C✝ D
X : Type u
inst✝ : TopologicalSpace X
C : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
mapsTo_iff_image_subset :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
union' : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)

Tactic:
simpa only [empty_union]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D : Set X✝
inst✝¹ : RelCWComplex C✝ D
X : Type u
inst✝ : TopologicalSpace X
C : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
mapsTo_iff_image_subset :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
union' : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ∅ ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C

Tactic:
simpa only [empty_union]

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[inferInstance, inst✝] (g ∘ ⇑f) ↔ Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)

Tactic:
simp [equiv, Equiv.refl]

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y

Tactic:
rw [sup_eq_iSup]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ π (π C K) J

Tactic:
dsimp [π]

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ Proj J '' Proj K '' C
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x✝ : (Finset I)ᵒᵖ
s : Finset I
⊢ (indexCone hC).π.app (op s) =
    (Iso.refl (indexCone hC).pt).hom ≫
      ((Cone.postcompose (spanFunctorIsoIndexFunctor hC).hom).obj (spanCone hC)).π.app (op s)

Tactic:
ext
      have : iso_map C (· ∈ s) ∘ ProjRestrict C (· ∈ s) = IndexFunctor.π_app C (· ∈ s) := by
        ext _ i; exact dif_pos i.prop
      exact congr_fun this.symm _

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)
⊢ ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) ∘ ProjRestrict (π C K) J = ⇑(eval (π C K) l)

Tactic:
← Function.comp_assoc,

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)
⊢ (⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯)) ∘ ProjRestrict (π C K) J = ⇑(eval (π C K) l)
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
y : β
⊢ ∃ z ∈ tβ, dist y z < ε₂

Tactic:
simpa using htβ (mem_univ y)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : ↑(MaxToGood C hC hsC ho h₁ m) = ↑(MaxToGood C hC hsC ho h₁ n)
⊢ ↑↑m = ↑↑n

Tactic:
dsimp [MaxToGood] at h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : (↑m).Tail = (↑n).Tail
⊢ ↑↑m = ↑↑n
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case neg
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hAU : A ⊆ ⋃ i, U i
h : IsEmpty ι
⊢ ∃ t, A ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨∅, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ ∀ t₁ ∈ range (Iic ∘ 𝓟), ∀ t₂ ∈ range (Iic ∘ 𝓟), ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range (Iic ∘ 𝓟), x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl

Goal state after:
α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ t₃ ∈ range (Iic ∘ 𝓟), l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ StronglyLocallyContractibleSpace (X × Y)

Tactic:
refine .of_bases (ι := Set X × Set Y)
    (p := fun (x, y) (Ux, Uy) =>
      (Ux ∈ 𝓝 x ∧ ContractibleSpace Ux) ∧ (Uy ∈ 𝓝 y ∧ ContractibleSpace Uy))
    (s := fun _ (Ux, Uy) => Ux ×ˢ Uy) ?_ ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ ∀ (x : X × Y),
    (𝓝 x).HasBasis
      (fun x_1 ↦
        match x with
        | (x, y) =>
          match x_1 with
          | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
      fun x ↦
      match x with
      | (Ux, Uy) => Ux ×ˢ Uy

case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ ∀ (x : X × Y) (i : Set X × Set Y),
    (match x with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
⊢ ∃ r, 1 ≤ r ∧ ↑(#({x ∈ V | edist t x ≤ ↑r * c})) ≤ a ^ r

Tactic:
have := ENNReal.tendsto_nhds_top_iff_nat.1
    ((ENNReal.tendsto_rpow_atTop_of_one_lt_base ha).comp tendsto_natCast_atTop_atTop) #V

Goal state after:
T : Type u_1
inst✝ : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
this : ∀ᶠ (a_1 : ℕ) in Filter.atTop, ↑(#V) < ((fun x ↦ a ^ x) ∘ Nat.cast) a_1
⊢ ∃ r, 1 ≤ r ∧ ↑(#({x ∈ V | edist t x ≤ ↑r * c})) ≤ a ^ r
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False

Tactic:
rcases hx with ⟨hxc, hx0⟩

Goal state after:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ cantorSet = (fun x ↦ x / 3) '' cantorSet ∪ (fun x ↦ (2 + x) / 3) '' cantorSet

Tactic:
simp only [cantorSet]

Goal state after:
⊢ ⋂ n, preCantorSet n = ((fun x ↦ x / 3) '' ⋂ n, preCantorSet n) ∪ (fun x ↦ (2 + x) / 3) '' ⋂ n, preCantorSet n
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ofDigits a ∈ preCantorSet 0

Tactic:
simp only [preCantorSet_zero, Set.mem_Icc]
    exact ⟨ofDigits_nonneg a, ofDigits_le_one a⟩

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

Tactic:
apply H.apply_zero

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Tactic:
intro l a ih

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d x z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z ∧ d' x z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z

Tactic:
refine ⟨(d.triangle x y z).trans ?_, (d'.triangle x y z).trans ?_⟩

Goal state after:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d x y + d y z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z

case refine_2
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d' x y + d' y z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝ : IsCompact s
this : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
⊢ hausdorffDist (Subtype.val '' range Φ') (Subtype.val '' range Ψ') = hausdorffDist (range Φ') (range Ψ')

Tactic:
exact hausdorffDist_image isometry_subtype_coe

Goal state after:
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y z : Snowflaking X α hα₀ hα₁
⊢ edist x z ≤ edist x y + edist y z

Tactic:
simp only [edist_def]
    grw [edist_triangle x.ofSnowflaking y.ofSnowflaking z.ofSnowflaking,
      ENNReal.rpow_add_le_add_rpow _ _ hα₀.le hα₁]

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
by_cases hU : U = univ

Goal state after:
case pos
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : U = univ
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

case neg
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ IsOpen[inst✝¹] U → U = univ ∨ ∃ a, (Iic a)ᶜ = U

pp: case mpr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ (U = univ ∨ ∃ a, (Iic a)ᶜ = U) → IsOpen[inst✝¹] U

Tactic:
· intro hU
    rcases eq_empty_or_nonempty Uᶜ with eUc | neUc
    · exact Or.inl (compl_empty_iff.mp eUc)
    · apply Or.inr
      use sSup Uᶜ
      rw [compl_eq_comm, le_antisymm_iff]
      refine ⟨fun _ ha ↦ le_sSup ha, (isLowerSet_of_isClosed hU.isClosed_compl).Iic_subset ?_⟩
      exact dirSupClosed_iff_forall_sSup.mp (dirSupClosed_of_isClosed hU.isClosed_compl) le_rfl neUc
        (isChain_of_trichotomous Uᶜ).directedOn

Goal state after:
case mpr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ (U = univ ∨ ∃ a, (Iic a)ᶜ = U) → IsOpen[inst✝¹] U
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
F : Set α
hF : F.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure F))ᶜ = R
⊢ ∃ a, (hull T a)ᶜ = R

Tactic:
lift F to Finset α using hF.1

Goal state after:
case mpr
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
F : Finset α
hF : (↑F).Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure ↑F))ᶜ = R
⊢ ∃ a, (hull T a)ᶜ = R
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h✝ : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
x : X
h : x ∉ s
i : ℕ
hi : x ∈ (U i)ᶜ
j : ℕ
hj : j ≠ i
⊢ 0 ≤ (f j) x * (1 / 2 / 2 ^ j)

Tactic:
positivity [(hfr j x).1]

Goal state after:
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : ToType (𝒢.obj (op U))
⊢ ∃ a, (ConcreteCategory.hom ((stalkFunctor C x).map T)) a = (ConcreteCategory.hom (𝒢.germ U x hxU)) t

Tactic:
rcases hT.imageSieve_mem t x hxU with ⟨V, ι, ⟨s, h_eq⟩, hxV⟩

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : ToType (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
h_eq : (ConcreteCategory.hom (T.app (op V))) s = (ConcreteCategory.hom (𝒢.map ι.op)) t
⊢ ∃ a, (ConcreteCategory.hom ((stalkFunctor C x).map T)) a = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
⊢ IsLocallySurjective T

Tactic:
constructor
    intro U t x hxU
    set t_x := 𝒢.germ _ x hxU t with ht_x
    obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
    obtain ⟨V, hxV, s, rfl⟩ := ℱ.exists_germ_eq s_x
    -- rfl : ℱ.germ x s = s_x
    have key_W := 𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
      convert! hs_x using 1
      symm
      convert! stalkFunctor_map_germ_apply _ _ _ _ s
    obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W
    refine ⟨W, hWU, ⟨ℱ.map hWV.op s, ?_⟩, hxW⟩
    convert! h_eq using 1
    simp only [← ConcreteCategory.comp_apply, T.naturality]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
⊢ ∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ

Tactic:
let M := ⌊ε⁻¹ * max C 0⌋₊

Goal state after:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
⊢ ∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i j : ι
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) } =
    ((Pi.lift fun i ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) }

Tactic:
simpa [SheafConditionEqualizerProducts.leftRes]
            using! c.π.naturality (Quiver.Hom.op (Hom.left i j))

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : Cb X Y
C : ℝ
⊢ BddAbove (range fun y ↦ ⨅ x, f (inl x, inr y) + C)

Tactic:
by
  obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove
  refine ⟨Cf + C, forall_mem_range.2 fun y => ?_⟩
  calc
    ⨅ x, f (inl x, inr y) + C ≤ f (inl default, inr y) + C := ciInf_le (HD_below_aux2 C) default
    _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

Goal state after: