mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
hmas : ↑m ≤ as
⊢ Products.eval (π C fun x ↦ x ∈ s) ⟨a :: ↑m, ⋯⟩ = e (π C fun x ↦ x ∈ s) a * Products.eval (π C fun x ↦ x ∈ s) m

Tactic:
simp only [Products.eval, List.map, List.prod_cons]

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

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
h : X.str F = x
s : Set X.A
hx : x ∈ s
hs : IsOpen s
⊢ X.str F ∈ s

Tactic:
h

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
h : X.str F = x
s : Set X.A
hx : x ∈ s
hs : IsOpen s
⊢ x ∈ s
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
⊢ ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Tactic:
h

Goal state after:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
⊢ ↑a i = ↑b i

Tactic:
by_cases hi : J i

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : J i
⊢ ↑a i = ↑b i

case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : ¬J i
⊢ ↑a i = ↑b i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case cons
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.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 : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (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 ≤ a :: as})

Tactic:
Finsupp.mem_span_image_iff_linearCombination

Goal state after:
case cons
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 :
  ∃ l ∈ Finsupp.supported ℤ ℤ {m | ↑m ≤ as},
    (Finsupp.linearCombination ℤ (Products.eval (π C fun x ↦ x ∈ s))) l =
      (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
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (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 ≤ a :: as})
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 Y : (Finset I)ᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    ((Functor.const (Finset I)ᵒᵖ).obj (of ↑C)).map f ≫
        ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop Y, continuous_toFun := ⋯ } =
      ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
        (spanFunctor hC).map f

Tactic:
h

Goal state after:
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 Y : (Finset I)ᵒᵖ
h : X ⟶ Y
⊢ ((Functor.const (Finset I)ᵒᵖ).obj (of ↑C)).map h ≫
      ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop Y, continuous_toFun := ⋯ } =
    ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
      (spanFunctor hC).map h
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
⊢ eval C ⟨a, ha⟩ = eval C ⟨b, hb⟩ → ⟨a, ha⟩ = ⟨b, hb⟩

Tactic:
h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : eval C ⟨a, ha⟩ = eval C ⟨b, hb⟩
⊢ ⟨a, ha⟩ = ⟨b, hb⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ Function.Injective (eval C)

Tactic:
intro ⟨a, ha⟩ ⟨b, hb⟩ h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : eval C ⟨a, ha⟩ = eval C ⟨b, hb⟩
⊢ ⟨a, ha⟩ = ⟨b, hb⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨b, hb⟩ < ⟨a, ha⟩
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})

Tactic:
h

Goal state after:
case inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨b, hb⟩ < ⟨a, ha⟩
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
⊢ compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝ → a₁✝ = a₂✝

Tactic:
h

Goal state after:
X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
⊢ isGood {fun x ↦ false} nil

Tactic:
by
  intro h
  simp [Products.eval, Products.nil] at h

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
⊢ (∀ y < l, L y) → L l

Tactic:
h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
⊢ L l
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j ∪ openCell l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

Tactic:
rcases hxj with hxj | hxj

Goal state after:
case h.inr.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

case h.inr.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ openCell l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
a b : ↑S.toTop
⊢ ι S a = ι S b → a = b

Tactic:
h

Goal state after:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
⊢ a = b
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_1
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
⊢ Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

pp: case refine_2
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 fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
⊢ Products.isGood C l

Tactic:
· by_cases hh : term I ho ∈ l.val
    · exact Or.inr ⟨h, hh⟩
    · left
      intro he
      apply h
      have h' := Products.prop_of_isGood_of_contained C _ h hsC
      simp only [Order.lt_succ_iff] at h'
      have hh' : ∀ a ∈ l.val, ord I a < o := by
        intro a ha
        refine (h' a ha).lt_of_ne ?_
        rw [ne_eq, ord_term ho a]
        rintro rfl
        contradiction
      rwa [Products.eval_πs_image C hh', ← Products.eval_πs C hh',
        Submodule.apply_mem_span_image_iff_mem_span (injective_πs _ _)]

Goal state after:
case refine_2
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 fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
⊢ Products.isGood C l
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
inst✝ : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
rw [empty_union]; exact union

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ∃ i, ↑i < ↑n + 1 ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
refine ⟨n, (by norm_cast; exact lt_add_one n), ⟨j,xmem⟩⟩

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✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
by
    obtain (hy | hy) := finite_or_infinite (ConnectedComponents X)
    · cases nonempty_fintype (ConnectedComponents X)
      simp only [ENat.card_eq_coe_fintype_card]
      refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [hij])) ?_
      · exact (isClopen_discrete _).preimage continuous_coe
      · exact (Set.singleton_nonempty _).preimage surjective_coe
      · simp [← Set.preimage_iUnion]
    · simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]
      intro m
      obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)
      exact le_trans (by simp) (h U hU1 hU2 hU3 hU4)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : ⇑f '' K ⊆ ⋃ i ∈ {s | s ∈ T ∧ s ⊆ U}, i
t : Set (Set Y)
ht : t ⊆ {s | s ∈ T ∧ s ⊆ U}
hfin : t.Finite
htK : ⇑f '' K ⊆ ⋃ i ∈ t, i
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t

Tactic:
refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : ⇑f '' K ⊆ ⋃ i ∈ {s | s ∈ T ∧ s ⊆ U}, i
t : Set (Set Y)
ht : t ⊆ {s | s ∈ T ∧ s ⊆ U}
hfin : t.Finite
htK : ⇑f '' K ⊆ ⋃ i ∈ t, i
⊢ ⇑f '' K ⊆ ⋃₀ t
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)
⊢ MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n → m = n

Tactic:
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 : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ m = n
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 : (↑m).Tail = (↑n).Tail
⊢ term I ho :: ↑(↑m).Tail = term I ho :: ↑(↑n).Tail

Tactic:
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
⊢ term I ho :: ↑(↑n).Tail = term I ho :: ↑(↑n).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]

Goal state after:
ι : 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
⊢ (∀ ⦃i : ι⦄ (f : C(X i, Z)) (i_1 : ι) (f_1 : C(X i_1, Y)), Continuous[inst✝⁴ i, _] (precomp f_1 ∘ g ∘ ⇑f)) ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : C(X i₁, Z)) ⦃i₂ : ι⦄ (f₂ : C(X i₂, Y)),
      Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦ (g (f₁ x.1)) (f₂ x.2)
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
u : Set X
⊢ IsOpen[t] u → IsOpen[⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace] u

Tactic:
h

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ IsOpen[⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace] u
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
⊢ Function.Injective ⇑(productOfMemOpens X)

Tactic:
intro x1

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 : X
⊢ ∀ ⦃a₂ : X⦄, (productOfMemOpens X) x1 = (productOfMemOpens X) a₂ → x1 = a₂
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
⊢ (productOfMemOpens X) x1 = (productOfMemOpens X) x2 → x1 = x2

Tactic:
h

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ x1 = x2
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable ((productOfMemOpens X) x1) ((productOfMemOpens X) x2)

Tactic:
h

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable ((productOfMemOpens X) x2) ((productOfMemOpens X) x2)
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' V)

Tactic:
refine continuous_subtype_val.isOpen_preimage _ ?_

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ IsOpen[inst✝²] V
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x_1 ↦ x - 3⁻¹ ^ x_1 - x) Filter.atTop (nhds 0)

Tactic:
simp only [sub_sub_cancel_left]

Goal state after:
case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x ↦ -3⁻¹ ^ x) Filter.atTop (nhds 0)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Filter.map (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l

Tactic:
Filter.map_prod

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (Filter.map (fun a b ↦ (a, b).1 :: (a, b).2) (𝓝 a)).seq (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l
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 : X
⊢ ∀ (z : X), d x z ⊔ d' x z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z

Tactic:
z

Goal state after:
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 z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z
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 : X
⊢ ∀ (z : X), (d ⊔ d') x z ≤ (d ⊔ d') x y ⊔ (d ⊔ d') y z

Tactic:
z

Goal state after:
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 ⊔ d') x z ≤ (d ⊔ d') x y ⊔ (d ⊔ d') y z
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: 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 : X
⊢ ∀ (z : X), (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)

Tactic:
z

Goal state after:
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
⊢ (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)
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 {p | edist p.1 p.2 < δ} (s, t).1

Tactic:
conv => enter [2, 2, 1, 1, _]; rw [edist_comm]

Goal state after:
α : 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
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
δ : ℝ≥0∞
hδ : 0 < δ
hδε : δ < ε
a✝ : Set α × Set α
⊢ a✝ ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ} → hausdorffEDist a✝.1 a✝.2 < ε

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
δ : ℝ≥0∞
hδ : 0 < δ
hδε : δ < ε
a✝ : Set α × Set α
h : a✝ ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ hausdorffEDist a✝.1 a✝.2 < ε