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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
| Set.univ ∩ f ⁻¹' {y}

Tactic:
← hU4,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
| (⋃ i, U i) ∩ f ⁻¹' {y}
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
h : Products.eval (C' C ho) (↑l).Tail ∈ Submodule.span ℤ (Products.eval (C' C ho) '' {m | m < (↑l).Tail})
⊢ False

Tactic:
rw [Finsupp.mem_span_image_iff_linearCombination, ← max_eq_eval C hsC ho] 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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
h :
  ∃ l_1 ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail},
    (Finsupp.linearCombination ℤ (Products.eval (C' C ho))) l_1 = (Linear_CC' C hsC ho) (Products.eval C ↑l)
⊢ False
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
p : Products I
hp : ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m q • Products.eval (C' C ho) q = m q • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑q)).prod

Tactic:
hp.2.2,

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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
p : Products I
hp : ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m p.Tail • Products.eval (C' C ho) p.Tail =
    m p.Tail • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑p.Tail)).prod
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
⊢ IsCountablyCompact A ↔ IsCountablyCompact (f '' A)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot Fc F_le => ?_⟩

Goal state after:
E : Type u_2
F✝ : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F✝
A : Set E
f : E → F✝
hf : IsInducing f
hs : IsCountablyCompact (f '' A)
F : Filter E
F_ne_bot : F.NeBot
Fc : F.IsCountablyGenerated
F_le : F ≤ 𝓟 A
⊢ ∃ a ∈ A, ClusterPt a F
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
hA : IsSeqCompact A
x : ℕ → F
hx : ∀ (n : ℕ), x n ∈ f '' A
⊢ ∃ a ∈ f '' A, ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
choose y hy using hx

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
hA : IsSeqCompact A
x : ℕ → F
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
⊢ ∃ a ∈ f '' A, ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Module: Mathlib.Topology.Instances.PNat

Goal state before:
pp: n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' closedBall (↑n) r)

Tactic:
Nat.closedBall_eq_Icc

Goal state after:
n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' Set.Icc ⌈↑↑n - r⌉₊ ⌊↑↑n + r⌋₊)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this✝ : IsClosed ({i}.domRestrict '' s)
this : ⇑(Homeomorph.piUnique fun t ↦ α ↑t) ∘ {i}.domRestrict = fun x ↦ x i
⊢ IsClosed ((fun x ↦ x i) '' s)

Tactic:
← this,

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this✝ : IsClosed ({i}.domRestrict '' s)
this : ⇑(Homeomorph.piUnique fun t ↦ α ↑t) ∘ {i}.domRestrict = fun x ↦ x i
⊢ IsClosed (⇑(Homeomorph.piUnique fun t ↦ α ↑t) ∘ {i}.domRestrict '' s)
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝² : AddCommMonoid R
inst✝¹ : LinearOrder R
inst✝ : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
⊢ 0 ≤ d x y

Tactic:
by_contra! H

Goal state after:
X : Type u_1
R : Type u_2
inst✝² : AddCommMonoid R
inst✝¹ : LinearOrder R
inst✝ : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : d x y < 0
⊢ False
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto (fun p ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 ((a' :: l).insertIdx (n + 1) a))

Tactic:
rw [this, tendsto_map'_iff]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun p ↦ p.2.insertIdx (n + 1) p.1) ∘ fun p ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
    (𝓝 ((a' :: l).insertIdx (n + 1) a))
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
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
x y z : X
⊢ d x z ⊔ d' x z ≤ d x y ⊔ d' x y ⊔ (d y z ⊔ d' y z)

Tactic:
calc d x z ⊔ d' x z ≤ d x y ⊔ d y z ⊔ (d' x y ⊔ d' y z) := sup_le_sup le_sup le_sup
  _ ≤ d x y ⊔ d' x y ⊔ (d y z ⊔ d' y z) := by simp [sup_comm, sup_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
⊢ (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {x | edist x.2 x.1 < δ} (s, t).1

Tactic:
have {s t : Set α} (h : ⨆ x ∈ s, infEDist x t < δ) :
      s ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} t := by
    intro x hx
    simpa only [infEDist, iInf_lt_iff, exists_prop] using! (le_iSup₂ x hx).trans_lt h

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
this : ∀ {s t : Set α}, ⨆ x ∈ s, infEDist x t < δ → s ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} t
⊢ (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {x | edist x.2 x.1 < δ} (s, t).1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
exact h.symm

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

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
exact h.symm

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

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
exact h.symm

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

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
exact h.symm

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

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
this : ↑(#J) ≤ 1
⊢ #J ≤ 1

Tactic:
norm_cast at this

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ ↑ε
a : X
ha : a ∈ A
⊢ {a} ⊆ A

Tactic:
simp [ha]

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ ↑ε
⊢ coveringNumber ε A ≤ 1

Tactic:
have ⟨a, ha⟩ := h_nonempty
    calc coveringNumber ε A
      _ ≤ ({a} : Set X).encard :=
        (IsCover.singleton_of_ediam_le hA ha).coveringNumber_le_encard (by simp [ha])
      _ ≤ 1 := by simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
⊢ IsClosed (candidatesB X Y)

Tactic:
have I4 : ∀ x y z, IsClosed { f : Cb X Y | f (x, z) ≤ f (x, y) + f (y, z) } := fun x y z =>
    isClosed_le (continuous_eval_const _) ((continuous_eval_const _).add (continuous_eval_const _))

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
⊢ IsClosed (candidatesB X Y)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
a : X
ha : a ∈ A
⊢ {a} ⊆ A

Tactic:
simp [ha]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)

Tactic:
have main : ∀ n : ℕ, edist (s n) t ≤ 2 * B n := fun n =>
    hausdorffEDist_le_of_mem_edist (I1 n) (I2 n)

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
C : ℝ≥0
hX : ∀ (x y : X), edist x y ≤ ↑C
this✝ : PseudoMetricSpace X := PseudoEMetricSpace.toPseudoMetricSpace ⋯
this : BoundedSpace X
⊢ MemHolder s f

Tactic:
exact hf.of_le hs

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
⊢ min (edist x y) (edist y x) ≤ {x, y}.einfsep

Tactic:
by
  simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]
  rintro a (rfl | rfl) b (rfl | rfl) hab <;> (try simp only [le_refl, true_or, or_true]) <;>
    contradiction

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

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

Tactic:
refine ⟨?_, isTopologicalBasis_insert_univ_subbasis.isOpen⟩

Goal state after:
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.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsOpen[t₁] s

Tactic:
rw [@isOpen_iff_isUpperSet α _ t₁]

Goal state after:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsUpperSet s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
⊢ Continuous[inst✝³, inst✝¹] ⇑f

Tactic:
refine IsLower.continuous_iff_Ici.2 fun b => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
⊢ IsClosed[inst✝³] (⇑f ⁻¹' Ici b)
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
⊢ ∀ (s t : Set (PT L)), (∃ u, {x | x u} = s) → (∃ u, {x | x u} = t) → ∃ u, {x | x u} = s ∩ t

Tactic:
by rintro s t ⟨u, rfl⟩ ⟨v, rfl⟩; use u ⊓ v; simp_rw [map_inf]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[L] s ↔ IsOpen[S] s

Tactic:
by
  rw [@IsLawson.topology_eq_lawson α _ L _, @IsScott.topology_eq α univ _ S _]
  exact lawsonOpen_iff_scottOpen_of_isUpperSet h

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist x z = dist (toGHSpace X) (toGHSpace Z)

Tactic:
rw [x.toGHSpace_rep, z.toGHSpace_rep]

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
K : Compacts α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
⊢ ⋯.functor.Initial

Tactic:
by
  rw [Monotone.initial_functor_iff]
  intro U
  obtain ⟨L, h1, h2, h3⟩ := exists_compact_between K.isCompact U.val.isOpen U.property
  use ⟨⟨interior L, isOpen_interior⟩,
    ⟨IsCompact.of_isClosed_subset h1 isClosed_closure
      (closure_minimal interior_subset (IsCompact.isClosed h1)),
    h2⟩⟩
  exact Subset.trans interior_subset h3

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
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ 𝓕.map ((OpenNhds.inclusion p₀).op.map inc) ≫ f.app (op ((OpenNhds.inclusion p₀).obj (unop V))) =
    f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯

Tactic:
f.naturality,

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
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫
      (skyscraperPresheaf p₀ c).map ((OpenNhds.inclusion p₀).op.map inc) =
    f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ principalOpen x
this : IsOpen[inst✝²] ↑U
⊢ y ∈ U

Tactic:
rw [IsUpperSet.isOpen_iff_isUpperSet] at this

Goal state after:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ principalOpen x
this : IsUpperSet ↑U
⊢ y ∈ U
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
hpq' : ∀ (i j : Fin (N p)), (F p).snd i j = (F q).snd ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
⊢ (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩

Tactic:
rw [← hpq']

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

Goal state before:
pp: X : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Preorder X
inst✝³ : Topology.IsUpperSet X
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
F : X ⥤ C
P : (Opens X)ᵒᵖ ⥤ C
η : principals X ⋙ P ⟶ F
inst✝ : P.IsRightKanExtension η
γ : principals X ⋙ principalsKanExtension F ⟶ F := (principals X).pointwiseRightKanExtensionCounit F
x✝ : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
this : P ≅ principalsKanExtension F
⊢ TopCat.Presheaf.IsSheaf P

Tactic:
isSheaf_iso_iff this

Goal state after:
X : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Preorder X
inst✝³ : Topology.IsUpperSet X
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
F : X ⥤ C
P : (Opens X)ᵒᵖ ⥤ C
η : principals X ⋙ P ⟶ F
inst✝ : P.IsRightKanExtension η
γ : principals X ⋙ principalsKanExtension F ⟶ F := (principals X).pointwiseRightKanExtensionCounit F
x✝ : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
this : P ≅ principalsKanExtension F
⊢ TopCat.Presheaf.IsSheaf (principalsKanExtension F)
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case refine_1
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
T : ℱ ⟶ 𝒢
h : IsLocallySurjective T
x✝ : Opens ↑X
t : ToType (𝒢.obj (op x✝))
x : ↑X
hx : x ∈ x✝
⊢ ∃ V, ∃ (x_1 : V ≤ x✝), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V

Tactic:
obtain ⟨V, i, hi⟩ := h.imageSieve_mem t x hx
    exact ⟨V, leOfHom i, hi⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map WalkingParallelPairHom.right ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map WalkingParallelPairHom.right

Tactic:
dsimp [diagram]

Goal state after:
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ rightRes F U ≫ (Pi.mapIso fun x ↦ α.app (op (U x.1 ⊓ U x.2))).hom =
    (Pi.mapIso fun x ↦ α.app (op (U x))).hom ≫ rightRes G U
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:
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:
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)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
hpq' : ∀ (i j : Fin (N p)), (F p).snd i j = (F q).snd ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
⊢ ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩)

Tactic:
rw [← hpq']

Goal state after: