mathlib-initiative/mathlib-tactics huggingface dataset:
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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
a : I
ha : a ∈ ↑l
⊢ ord I a ≠ o

Tactic:
ne_eq,

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
a : I
ha : a ∈ ↑l
⊢ ¬ord I a = o
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
l : ℕ
hln : ↑l < n
i : cell C l
⊢ Disjoint (openCell l i) (openCell m j)

Tactic:
apply disjoint_openCell_of_ne

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
l : ℕ
hln : ↑l < n
i : cell C l
⊢ ⟨l, i⟩ ≠ ⟨m, j⟩
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ ⋂ n, dissipate C n = ∅
f : ∀ (n : ℕ), dissipate C n ∈ S
⊢ ∃ n, dissipate C n = ∅

pp: case neg
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ ⋂ n, dissipate C n = ∅
f : ∃ n, dissipate C n ∉ S
⊢ ∃ n, dissipate C n = ∅

Tactic:
· exact h (dissipate C) directed_dissipate f this.2

Goal state after:
case neg
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ ⋂ n, dissipate C n = ∅
f : ∃ n, dissipate C n ∉ S
⊢ ∃ n, dissipate C n = ∅
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ ofCompactSupport (⇑g * ⇑↑f) ⋯ ⋯ ∈ C_cb(α, γ)

Tactic:
apply mem_compactlySupported.mpr

Goal state after:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ HasCompactSupport ⇑(ofCompactSupport (⇑g * ⇑↑f) ⋯ ⋯)
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact (F ⁻¹' A)

pp: case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
⊢ f ∈ comp Subtype.val M '' F ⁻¹' A

Tactic:
· have : CompactSpace s := isCompact_iff_compactSpace.1 hs
    refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_
    rw [isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff]
    exact H.comp (A.restrictPreimage F)

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
⊢ f ∈ comp Subtype.val M '' F ⁻¹' A
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)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
⊢ LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail

Tactic:
have hh : (fun l ↦ Products.eval (C' C ho) l.val.Tail) = eval (C' C ho) ∘ f := rfl

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)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun l ↦ Products.eval (C' C ho) (↑l).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i : ι), LocallyCompactSpace (X i)
g : Z → ContinuousMapGeneratedBy X Y T
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : C(X i₁, Z)) ⦃i₂ : ι⦄ (f₂ : C(X i₂, Y)),
      Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
        match x with
        | (x₁, x₂) => (g (f₁ x₁)) (f₂ x₂)

Tactic:
simp only [continuousGeneratedBy_def, continuous_iff]
  exact forall_congr' (fun i₁ ↦ forall_congr' (fun f₁ ↦
    forall_congr' (fun i₂ ↦ forall_congr' (fun f₂ ↦
      ⟨fun h ↦ ContinuousMap.continuous_uncurry_of_continuous ⟨_, h⟩,
        fun h ↦ (ContinuousMap.curry ⟨_, h⟩).continuous⟩))))

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case succ
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius

Tactic:
by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius

case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
h : (logSizeBallSeq J hJ a c (i + 1)).finset = ∅
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))

Tactic:
by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))

case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset = ∅
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a →
      ↑(#J) ≤ a ^ n →
        ∀ {s t : T},
          (s, t) ∈ pairSet J a c → ∀ i < #J, (s, t) ∈ pairSetSeq J a c i → J.Nonempty → 1 ≤ n → edist s t ≤ ↑n * c
hn : n < 1
⊢ edist s t ≤ ↑n * c

pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
n✝ : ℕ
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
hn : 1 ≤ n
⊢ edist s t ≤ ↑n * c

Tactic:
· suffices s = t by simp [this]
    simp only [Nat.lt_one_iff.mp hn, pow_zero, Nat.cast_le_one] at hJ_card
    have ⟨hs, ht⟩ := Finset.mem_product.mp (pairSet_subset h)
    exact Finset.card_le_one_iff.mp hJ_card hs ht

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
n✝ : ℕ
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
hn : 1 ≤ n
⊢ edist s t ≤ ↑n * c
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_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (0, x_1) =
      (toLoop i p).toContinuousMap x_1

pp: case refine_4
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_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

pp: case refine_5
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)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ?refine_3,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
iterate 2
    intro
    ext
    dsimp
    rw [homotopyTo_apply, toLoop_apply]
    swap

Goal state after:
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✝))

case refine_4
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 ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))

case refine_5
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)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case e_a
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑(logSizeBallSeq J hJ a c l).radius - 1 + 1 = ↑(logSizeBallSeq J hJ a c l).radius

Tactic:
ENNReal.sub_add_eq_add_sub _ (ENNReal.one_ne_top),

Goal state after:
case e_a
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑(logSizeBallSeq J hJ a c l).radius + 1 - 1 = ↑(logSizeBallSeq J hJ a c l).radius

T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ ↑(logSizeBallSeq J hJ a c l).radius
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_eq_empty : A = ∅
⊢ coveringNumber ε A ≤ 1

Tactic:
rw [← coveringNumber_eq_zero (ε := ε)] at h_eq_empty

Goal state after:
case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_eq_empty : coveringNumber ε A = 0
⊢ coveringNumber ε A ≤ 1
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

Tactic:
(try simp only [le_refl, true_or, or_true])

Goal state after:
case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b

Tactic:
(try simp only [le_refl, true_or, or_true])

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

Tactic:
(try simp only [le_refl, true_or, or_true])

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b

Tactic:
(try simp only [le_refl, true_or, or_true])

Goal state after:
case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case univ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsLowerSet univ

Tactic:
exact isLowerSet_univ

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

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen[inst✝¹] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s

Tactic:
rw [topology_eq α D]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ instTopologicalSpaceProd = lower (α × β)

Tactic:
by
    refine le_antisymm (le_generateFrom ?_) ?_
    · rintro _ ⟨x, rfl⟩
      exact (isClosed_Ici.prod isClosed_Ici).isOpen_compl
    rw [(IsLower.isTopologicalBasis.prod
      IsLower.isTopologicalBasis).eq_generateFrom, le_generateFrom_iff_subset_isOpen,
      image2_subset_iff]
    rintro _ ⟨s, hs, rfl⟩ _ ⟨t, ht, rfl⟩
    dsimp
    simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]
    -- without `let`, `refine` tries to use the product topology and fails
    let _ : TopologicalSpace (α × β) := lower (α × β)
    refine (hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)
    · exact GenerateOpen.basic _ ⟨(a, ⊥), by simp [Ici_prod_eq, prod_univ]⟩
    · exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩

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

Goal state before:
pp: case e'_5.inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
U : TopologicalSpace.Opens ↑X
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
⊢ s.arrows (𝟙 ⊤)

Tactic:
obtain rfl | rfl := U.eq_bot_or_top

Goal state after:
case e'_5.inr.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊥ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊥
⊢ s.arrows (𝟙 ⊤)

case e'_5.inr.inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊤ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊤
⊢ s.arrows (𝟙 ⊤)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ (skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U ≫ eqToHom ⋯ ≫ c.ι.app (op ⊤) = c.ι.app U

Tactic:
by
    dsimp
    rw [← c.w (homOfLE <| (le_top : unop U ≤ _)).op]
    change _ ≫ _ ≫ dite _ _ _ ≫ _ = _
    rw [dif_pos]
    · simp only [eqToHom_trans_assoc,
        eqToHom_refl, Category.id_comp, op_unop]
    · exact h.mem_open U.unop.1.2 U.unop.2

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

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h✝ : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).pt ⟶ c.pt
h : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).ι.app j ≫ f = c.ι.app j
⊢ f = eqToHom ⋯ ≫ (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).ι.app (op ⊤) ≫ f

Tactic:
skyscraperPresheafCoconeOfSpecializes_ι_app,

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h✝ : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).pt ⟶ c.pt
h : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).ι.app j ≫ f = c.ι.app j
⊢ f = eqToHom ⋯ ≫ eqToHom ⋯ ≫ f
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case pos
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 ≤ ε
p : GHSpace
hp : p ∉ t
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

pp: case neg
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 ≤ ε
p : GHSpace
hp : ¬p ∉ t
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

Tactic:
· have : Nonempty (Equiv (∅ : Set p.Rep) (Fin 0)) := by
        rw [← Fintype.card_eq, card_empty, Fintype.card_fin]
      use ∅, 0, bot_le, this.some
      exact fun hp' => (hp hp').elim

Goal state after:
case neg
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 ≤ ε
p : GHSpace
hp : ¬p ∉ t
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i =
    c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i

Tactic:
rw [← f.w WalkingParallelPair.zero, Category.assoc]

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
t : F.stalk x
⊢ ∃ U f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = t

Tactic:
obtain ⟨U, m, s, rfl⟩ := F.exists_germ_eq t

Goal state after:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ U_1 f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s