mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
this : ∀ (m : ℕ) (j : cell C m), m < n
f : (m : { m // m < n }) × cell C ↑m ≃ (m : ℕ) × cell C m :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨↑m, j⟩,
    invFun := fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨⟨m, ⋯⟩, j⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ _root_.Finite ((m : { m // m < n }) × cell C ↑m)

Tactic:
exact Finite.instSigma

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic (A ∩ B) → G ∈ basic A ∩ basic B

Tactic:
intro hG
    constructor <;> filter_upwards [hG] with _
    exacts [And.left, And.right]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
⊢ Disjoint (openCell n i) D ∧ Disjoint (openCell n i) (⋃ n, ⋃ j, openCell n ↑j)

Tactic:
disjoint_iUnion_right

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
⊢ Disjoint (openCell n i) D ∧ ∀ (i_1 : ℕ) (i_2 : ↑(J i_1)), Disjoint (openCell n i) (openCell i_1 ↑i_2)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
⊢ T2Space X.A

Tactic:
t2_iff_ultrafilter

Goal state after:
X : Compactum
⊢ ∀ {x y : X.A} (f : Ultrafilter X.A), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ih :
  List.IsChain (fun x1 x2 ↦ x1 > x2) as →
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ as})
ha : (∀ y ∈ as.head?, a > y) ∧ List.IsChain (fun x1 x2 ↦ x1 > x2) as
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) as

Tactic:
exact ha.2

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: ⊢ CreatesLimits (forget Profinite)

Tactic:
change CreatesLimits (profiniteToCompHaus ⋙ forget _)

Goal state after:
⊢ CreatesLimits (profiniteToCompHaus ⋙ forget CompHaus)
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x ↦ ord I x < o)
b : Products I
hb : b ∈ MaxProducts C ho
hab : a = b
⊢ False

Tactic:
← hab

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x ↦ ord I x < o)
b : Products I
hb : a ∈ MaxProducts C ho
hab : a = b
⊢ False
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 : ℕ
j : cell C n
⊢ closedCell n j ⊆ ↑(skeletonLT C (↑n + 1))

Tactic:
intro x xmem
  rw [coe_skeletonLT]
  right
  simp_rw [mem_iUnion, exists_prop]
  refine ⟨n, (by norm_cast; exact lt_add_one n), ⟨j,xmem⟩⟩

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
⊢ finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1

Tactic:
by simp [h]

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

Goal state before:
pp: case pos
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ ↑x i ≠ true
⊢ False

Tactic:
exact hi.2 (h₃ i hi.1)

Goal state after:
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✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace ↑(connectedComponent y)
⊢ ((connectedComponent y).restrictPreimage f ⁻¹' {⟨y, ⋯⟩}).Finite

Tactic:
rw [← Set.finite_image_iff Subtype.val_injective.injOn]

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✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace ↑(connectedComponent y)
⊢ (Subtype.val '' (connectedComponent y).restrictPreimage f ⁻¹' {⟨y, ⋯⟩}).Finite
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
x : γ
hx : x ≠ 0
⊢ const α x ∈ C_cb(α, γ)

Tactic:
by simp [h]

Goal state after:
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
this : CompactSpace ↑s
⊢ IsCompact (F ⁻¹' A)

Tactic:
refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_

Goal state after:
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
this : CompactSpace ↑s
⊢ Equicontinuous fun x ↦ ⇑↑x
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 : ↑(MaxProducts C ho)
⊢ ∀ ⦃a₂ : ↑(MaxProducts C ho)⦄, MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ a₂ → m = a₂

Tactic:
n

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)
⊢ MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n → m = n
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := ⋯
⊢ (⋃ U, range fun n ↦ Subtype.val '' (K U) n).Countable ∧
    (∀ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, IsCompact K_1) ∧
      ∀ (f : C(X, Y)) (V : Set Y),
        IsOpen[inst✝³] V →
          ∀ x ∈ ⇑f ⁻¹' V, ∃ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, K_1 ∈ 𝓝 x ∧ MapsTo (⇑f) K_1 V

Tactic:
refine ⟨countable_iUnion fun _ ↦ countable_range _, ?_, ?_⟩

Goal state after:
case h.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, IsCompact K_1

case h.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst✝³] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, K_1 ∈ 𝓝 x ∧ MapsTo (⇑f) K_1 V
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)
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X (Y × Z) T
⊢ ContinuousGeneratedBy X fun z ↦ g.comp { toFun := fun y ↦ (y, z), prop := ⋯ }

Tactic:
by
        simpa only [continuousGeneratedBy_iff_uncurry,
          continuousGeneratedBy_dom_prod_iff] using! g.prop

Goal state after:
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)
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)
⊢ ContinuousGeneratedBy X fun x ↦ (g x.2) x.1

Tactic:
by
        simpa only [continuousGeneratedBy_iff_uncurry,
          continuousGeneratedBy_dom_prod_iff] using! g.prop

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x ↦ ↑x
⊢ (f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩

Tactic:
have : PreconnectedSpace s := Subtype.preconnectedSpace hs

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x ↦ ↑x
this : PreconnectedSpace ↑s
⊢ (f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace ↑(s x i)
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ ContractibleSpace ↑s) id

Tactic:
rw [hasBasis_self]
    intro t ht
    obtain ⟨i, hpi, hi⟩ := (h x).mem_iff.mp ht
    exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

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

Goal state before:
pp: case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a → J.Nonempty → ↑(#(pairSet J a c)) ≤ a * ↑(#J)
hJ : ¬J.Nonempty
⊢ ↑(#(pairSet J a c)) ≤ a * ↑(#J)

pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ↑(#(pairSet J a c)) ≤ a * ↑(#J)

Tactic:
· simp [Finset.not_nonempty_iff_eq_empty.mp hJ]

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ↑(#(pairSet J a c)) ≤ a * ↑(#J)
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✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
| ∑ i ∈ Finset.range #J,
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c i).radius - ?m.162 i + ?m.162 i)

Tactic:
enter [2]; ext _; rw [pow_add, pow_one, ← mul_assoc, mul_comm]

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
x✝ : ℕ
| a * ((if (logSizeBallSeq J hJ a c x✝).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c x✝).radius - 1))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ {
      toFun := fun t ↦
        ⟨(({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp
                (ContinuousMap.id (↑I × ({ j // j ≠ i } → ↑I)))).curry
            t,
          ⋯⟩,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    p

Tactic:
ContinuousMap.comp_id

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ { toFun := fun t ↦ ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    p
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ Summable fun i ↦ ‖ofDigitsTerm (cantorToTernary x).get i‖

Tactic:
simpa only [norm_of_nonneg ofDigitsTerm_nonneg] using summable_ofDigitsTerm

Goal state after:
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)

pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Tactic:
· exact ⟨H.continuous, H.universally_closed _⟩

Goal state after:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:

Tactic:
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.BundledFun

Goal state before:
pp: case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)

Tactic:
finsetSup_apply hs

Goal state after:
case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ (f i) x z) ≤ max (s.sup' hs fun i ↦ (f i) x y) (s.sup' hs fun i ↦ (f i) y z)
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
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
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
apply le_trans (edist_triangle _ (f (logSizeBallSeq J hJ a c l).point) _)

Goal state after:
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 := ⋯
l : ℕ := ⋯
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
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f ↑⟨s, hs⟩) (f (logSizeBallSeq J hJ a c l).point) +
      edist (f (logSizeBallSeq J hJ a c l).point) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤
    (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : A = ∅
⊢ ∀ i ⊆ A, IsSeparated (↑ε) i → i = ∅

Tactic:
by simp [h]

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ (∀ (x₁ x₂ : X), f x₁ = f x₂) → eHolderNorm r f = 0

Tactic:
· intro h
    rcases isEmpty_or_nonempty X with hX | hX
    · exact eHolderNorm_of_isEmpty
    · rw [← eHolderNorm_const X r (f hX.some)]
      congr
      simp [funext_iff, h _ hX.some]

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_

Goal state after:
case pos.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ ↑(nnHolderNorm r f * ‖c‖₊) ≤ ↑‖c‖₊ * eHolderNorm r f

case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r f ≤ eHolderNorm r (c • f) / ↑‖c‖₊
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
⊢ 0 < s.einfsep

Tactic:
rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
    exact hxy'.symm ▸ edist_pos.2 hxy

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
hb : ∀ i ∈ S, b ∈ iᶜ
⊢ b ∉ Iio c

Tactic:
← compl_Ici

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
hb : ∀ i ∈ S, b ∈ iᶜ
⊢ b ∉ (Ici c)ᶜ
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
a b : L
⊢ {x | x (a ⊓ b)} = {x | x a} ⊓ {x | x b}

Tactic:
simp [Set.ofPred_and]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
⊢ Continuous fun a ↦ principal a

Tactic:
OrderTopology.continuous_iff

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
⊢ ∀ (a : DedekindCut α), IsOpen ((fun a ↦ principal a) ⁻¹' Ioi a) ∧ IsOpen ((fun a ↦ principal a) ⁻¹' Iio a)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q < 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

Tactic:
· obtain ⟨y, hy⟩ := not_isSuccPrelimit_iff.1 <| mt hx₁ hq.not_ge
      convert isOpen_Ioi (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_right

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
⊢ kernel (hull T a) = a

Tactic:
conv_rhs => rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
⊢ kernel (hull T a) =
    OrderDual.ofDual (OrderDual.toDual ((⇑OrderDual.toDual ∘ kernel) ((hull T ∘ ⇑OrderDual.ofDual) a)))