mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap F
        (UniformSpace.comap (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))
          (UniformFun.uniformSpace (↑i) α)) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)

Tactic:
← UniformSpace.comap_comap,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ F)
        (UniformFun.uniformSpace (↑i) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
have H1 : (UniformOnFun.uniformSpace X α 𝔖).comap F =
      ⨅ (K ∈ 𝔖), (UniformFun.uniformSpace _ _).comap (K.domRestrict ∘ F) := by
    simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap,
      UniformFun.ofFun, Equiv.coe_fn_mk, UniformOnFun.toFun, UniformOnFun.ofFun, Function.comp_def,
      UniformFun, Equiv.coe_fn_symm_mk]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: case mpr
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := ⋯
S2 : Set (X →ₜ* Y) := ⋯
S3 : Set C(X, Y) := ⋯
S4 : Set (X → Y) := ⋯
h : Equicontinuous fun x ↦ ⇑↑x
x✝ : X → Y
⊢ x✝ ∈ DFunLike.coe '' S1 → x✝ ∈ S4

Tactic:
rintro ⟨f, hf, rfl⟩
      exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
E'' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
R : Type u_9
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
x : M
x✝ : ↑(mulFiber x)
p : M × M
h : p ∈ mulFiber x
⊢ p.swap ∈ mulFiber x

Tactic:
by simp_all [mem_mulFiber, mul_comm]

Goal state after:
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
⊢ (fun y ↦ 1 + y) x ∈ s

Tactic:
have := Ideal.mem_jacobson_bot.mp (hI (Ideal.pow_le_self hn hx)) 1

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (x * 1 + 1)
⊢ (fun y ↦ 1 + y) x ∈ s
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ (↑x).arg + (↑x).arg ∈ Set.Ioc (-π) π

Tactic:
apply Set.Ioo_subset_Ioc_self

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := ⋯
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ (↑x).arg + (↑x).arg ∈ Set.Ioo (-π) π
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : BorelSpace α
h : MeasurableSet s
this✝ : MeasurableSpace α := borel α
⊢ BaireMeasurableSet s

Tactic:
exact h.eventuallyMeasurableSet

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : CWComplex C
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A ↔ ∀ (n : ℕ) (j : cell C n), IsClosed[t] (A ∩ closedCell n j)

Tactic:
by
  have := RelCWComplex.closed C A asubc
  simp_all

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (if ∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true then 1 else 0) =
    if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Tactic:
simp +contextual [h, Proj]

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

Goal state before:
pp: case hi.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ (cellFrontier (n + 1) j ∪ openCell (n + 1) j))

Tactic:
inter_union_distrib_left

Goal state after:
case hi.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ cellFrontier (n + 1) j ∪ A ∩ openCell (n + 1) j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun x ↦ ord I x < o) g i = g i

Tactic:
simp only [Proj, ite_eq_left_iff, not_lt, @eq_comm _ false, ← Bool.not_eq_true]
    specialize hsC g hg.1 i
    intro h'
    contrapose! hsC
    exact ⟨hsC, Order.succ_le_of_lt (h'.lt_of_ne' h)⟩

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
i : I
h₁ : ord I i < o
h₂ : ord I i = o
⊢ true = ↑x i

Tactic:
exact (h₁.ne h₂).elim

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

Goal state before:
pp: case inl
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 : I → Bool
hx : x ∈ C0 C ho
i : I
hsC : x i = true → ord I i < Order.succ o
hi✝ : o ≤ ord I i
hi : o < ord I i
⊢ false = x i

Tactic:
rw [← not_imp_not] at hsC

Goal state after:
case inl
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 : I → Bool
hx : x ∈ C0 C ho
i : I
hsC : ¬ord I i < Order.succ o → ¬x i = true
hi✝ : o ≤ ord I i
hi : o < ord I i
⊢ false = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
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 : I → Bool
hx : x ∈ C1 C ho
i : I
hsC : x i = true → ord I i < Order.succ o
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
⊢ false = x i

Tactic:
rw [← not_imp_not] at hsC

Goal state after:
case neg
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 : I → Bool
hx : x ∈ C1 C ho
i : I
hsC : ¬ord I i < Order.succ o → ¬x i = true
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
⊢ false = x i
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 ∈ closedCell l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

Tactic:
rw [← cellFrontier_union_openCell_eq_closedCell] at hxj

Goal state after:
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
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
⊢ ∃ f', f' ≫ g = f

Tactic:
let h : Ultrafilter X → Y := Ultrafilter.extend t

Goal state after:
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
⊢ ∃ f', f' ≫ g = f
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
⊢ ↑(skeletonLT C n) ∩ (cellFrontier m j ∪ openCell m j) ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
inter_union_distrib_left

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
⊢ ↑(skeletonLT C n) ∩ cellFrontier m j ∪ ↑(skeletonLT C n) ∩ openCell m j ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
⊢ IsCompactSystem S

Tactic:
by
  intro C hC
  contrapose!
  exact h C hC

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.IsChain (fun x x_1 ↦ x > x_1) (term I ho :: ↑q)

Tactic:
rw [List.isChain_iff_pairwise]

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 : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.Pairwise (fun x x_1 ↦ x > x_1) (term I ho :: ↑q)
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
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
i : Fin n
⊢ y ∈ f '' U i

Tactic:
convert! Set.mem_univ y

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
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
i : Fin n
⊢ f '' U i = Set.univ
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)))
⊢ Products.isGood (C' C ho) (↑l).Tail

Tactic:
by
  have : Inhabited I := ⟨term I ho⟩
  -- Write `l.Tail` as a linear combination of smaller products:
  intro h
  rw [Finsupp.mem_span_image_iff_linearCombination, ← max_eq_eval C hsC ho] at h
  obtain ⟨m, ⟨hmmem, hmsum⟩⟩ := h
  rw [Finsupp.linearCombination_apply] at hmsum
  -- Write the image of `l` under `Linear_CC'` as `Linear_CC'` applied to the linear combination
  -- above, with leading `term I ho`'s added to each term:
  have : (Linear_CC' C hsC ho) (l.val.eval C) = (Linear_CC' C hsC ho)
      (Finsupp.sum m fun i a ↦ a • ((term I ho :: i.1).map (e C)).prod) := by
    rw [← hmsum]
    simp only [map_finsuppSum]
    apply Finsupp.sum_congr
    intro q hq
    rw [map_smul]
    rw [Finsupp.mem_supported] at hmmem
    have hx'' : q < l.val.Tail := hmmem hq
    have : ∃ (p : Products I), p.val ≠ [] ∧ p.val.head! = term I ho ∧ q = p.Tail :=
      ⟨⟨term I ho :: q.val, isChain_cons_of_lt C hsC ho l q hx''⟩,
        ⟨List.cons_ne_nil _ _, by simp only [List.head!_cons],
        by simp only [Products.Tail, List.tail_cons, Subtype.coe_eta]⟩⟩
    obtain ⟨p, hp⟩ := this
    rw [hp.2.2, ← Products.max_eq_eval C hsC ho p hp.1 hp.2.1]
    dsimp [Products.eval]
    rw [Products.max_eq_o_cons_tail ho p hp.1 hp.2.1, List.map_cons, List.prod_cons]
  have hse := succ_exact C hC hsC ho
  rw [ShortComplex.moduleCat_exact_iff_range_eq_ker] at hse
  dsimp [ModuleCat.ofHom] at hse
  -- Rewrite `this` using exact sequence manipulations to conclude that a term is in the range of
  -- the linear map `πs`:
  rw [← LinearMap.sub_mem_ker_iff, ← hse] at this
  obtain ⟨(n : LocallyConstant (π C (ord I · < o)) ℤ), hn⟩ := this
  rw [eq_sub_iff_add_eq] at hn
  have hn' := h₁ (Submodule.mem_top : n ∈ ⊤)
  rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn'
  obtain ⟨w, hc⟩ := hn'
  rw [← hc, map_finsuppSum] at hn
  apply l.prop.1
  rw [← hn]
  -- Now we just need to prove that a sum of two terms belongs to a span:
  apply Submodule.add_mem
  · apply Submodule.finsuppSum_mem
    intro q _
    rw [map_smul]
    apply Submodule.smul_mem
    apply Submodule.subset_span
    dsimp only [eval]
    rw [Products.eval_πs C (Products.prop_of_isGood _ _ q.prop)]
    refine ⟨q.val, ⟨?_, rfl⟩⟩
    simp only [Products.lt_iff_lex_lt, Set.mem_ofPred_eq]
    exact good_lt_maxProducts C hsC ho q l
  · apply Submodule.finsuppSum_mem
    intro q hq
    apply Submodule.smul_mem
    apply Submodule.subset_span
    rw [Finsupp.mem_supported] at hmmem
    rw [← Finsupp.mem_support_iff] at hq
    refine ⟨⟨term I ho :: q.val, isChain_cons_of_lt C hsC ho l q (hmmem hq)⟩, ⟨?_, rfl⟩⟩
    simp only [Products.lt_iff_lex_lt, Set.mem_ofPred_eq]
    rw [max_eq_o_cons_tail C hsC ho l]
    exact List.Lex.cons ((Products.lt_iff_lex_lt q l.val.Tail).mp (hmmem hq))

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 : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
⊢ ⋂ L ∈ s, {g | MapsTo (⇑g) L (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}

Tactic:
simp only [← ofPred_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]

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 : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
⊢ {x | MapsTo (⇑x) (⋃₀ s) (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 1 γ = γ

Tactic:
simp only [delayReflLeft, delayReflRight_one, Path.symm_symm]

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case hf
⊢ Function.Bijective fun x ↦ x / 3

pp: ⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ ⋂ i, (fun x ↦ (2 + x) / 3) '' preCantorSet i

Tactic:
· exact mulRight_bijective₀ 3⁻¹ (by simp)

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

Goal state before:
pp: case hgf
x : ℝ
hx : x ∈ cantorSet
⊢ (fun n ↦ x - 3⁻¹ ^ n) ≤ fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i

pp: case hfh
x : ℝ
hx : x ∈ cantorSet
⊢ (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) ≤ fun x_1 ↦ x

Tactic:
· exact fun _ ↦ le_ofDigits_cantorToTernary_sum hx

Goal state after:
case hfh
x : ℝ
hx : x ∈ cantorSet
⊢ (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) ≤ fun x_1 ↦ x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
h : j ≠ i
⊢ Function.uncurry (fun x_1 y ↦ Function.uncurry (fun x_2 y ↦ (H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (t, y)) =
    ↑p y

Tactic:
rw [p.2 _ ⟨j, jH⟩]; apply boundary; exact ⟨⟨j, h⟩, jH⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := fun x ↦ ⟨⋯.choose, ⋯⟩
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ edist ↑x ↑(f x) + edist ↑(f x) ↑y ≤ 2 * ↑ε

Tactic:
rw [two_mul]
      gcongr
      · exact hf' x
      · simpa [edist_comm, hxy] using hf' y

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

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

Tactic:
intro h x₁ x₂

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
⊢ f x₁ = f x₂
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
· exact Or.inr (einfsep_le_edist_of_mem hy hz hyz)

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ eball x d = ⇑toSnowflaking '' eball (ofSnowflaking x) (d ^ α⁻¹)

Tactic:
image_toSnowflaking_eball,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ eball x d = eball (toSnowflaking (ofSnowflaking x)) ((d ^ α⁻¹) ^ α)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsClosed[inst✝¹] s ↔ IsLowerSet s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
    isLowerSet_compl.symm, compl_compl]

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

Goal state before:
pp: case h.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 : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
⊢ b ∈ ⋂₀ (compl '' S)

Tactic:
simp only [sInter_image, mem_iInter, mem_compl_iff]

Goal state after:
case h.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 : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
⊢ ∀ i ∈ S, b ∉ i