mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : f 0 = 0
⊢ n.factorization = q • (f.prod fun x1 x2 ↦ x1 ^ x2).factorization

Tactic:
n.factorization_prod_pow_eq_self_of_le_factorization ?_

Goal state after:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : f 0 = 0
⊢ n.factorization = q • f

n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : f 0 = 0
⊢ f ≤ n.factorization
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r

Tactic:
by
  simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
  exact (jacobiSym.div_four_left (mod_cast ha) hb).symm

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
xs ys : List α
h : xs ~ ys
h' : ys.Nodup
h₀ : xs.length ≤ ys.length
h₁ : ys.length ≤ xs.length
⊢ map Sigma.fst (List.toFinmap' (xs.zip ys)) ~ map Sigma.snd (List.toFinmap' (xs.zip ys))

Tactic:
simp only [List.toFinmap', comp_def, List.map_fst_zip, List.map_snd_zip, *,
        List.map_map]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
⊢ ProfiniteCompletion.eta G ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map (ProfiniteCompletion.lift (𝟙 G ≫ ProfiniteCompletion.eta G)) =
    ProfiniteCompletion.eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (𝟙 (ProfiniteCompletion.completion G))

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: X✝ Y✝ Z✝ : GrpCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ProfiniteCompletion.eta X✝ ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map (ProfiniteCompletion.lift ((f ≫ g) ≫ ProfiniteCompletion.eta Z✝)) =
    ProfiniteCompletion.eta X✝ ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map
        (ProfiniteCompletion.lift (f ≫ ProfiniteCompletion.eta Y✝) ≫
          ProfiniteCompletion.lift (g ≫ ProfiniteCompletion.eta Z✝))

Tactic:
cat_disch

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

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
⊢ ‖c‖ ^ (k + 1) ≤ 1

Tactic:
hc₁.le,

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
⊢ 1 ^ (k + 1) ≤ 1
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 + p.2

Tactic:
let t₁ : TopologicalSpace E := .induced (B · ·) Pi.topologicalSpace
    have : B.IsWeak := ⟨rfl⟩
    rw [hB.eq_induced, continuous_induced_rng]
    simp only [Function.comp_def, map_add, add_apply]
    fun_prop

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 • p.2

Tactic:
by
    let t₁ : TopologicalSpace E := .induced (B · ·) Pi.topologicalSpace
    have : B.IsWeak := ⟨rfl⟩
    rw [hB.eq_induced, continuous_induced_rng]
    simp only [Function.comp_def, map_smul, smul_apply]
    fun_prop

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ perfectKernel s = sᵈ[a]

Tactic:
refine le_antisymm (perfectKernel_subset_iteratedDerivedSet s a) ?_
  refine Set.subset_iInter fun i => ?_
  rcases lt_or_ge i a with hi | hi
  · exact iteratedDerivedSet_antitone s hi.le
  · exact (gfpApprox_eq_of_mem_fixedPoints relDerivedSet hi ha).ge

Goal state after:
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

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
g : Y → Z
hg : ContinuousGeneratedBy X g
⊢ Continuous (⇑WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑WithGeneratedByTopology.equiv)

Tactic:
rwa [← continuousGeneratedBy_iff]

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ Continuous ⇑WithGeneratedByTopology.equiv.symm

Tactic:
rw [continuous_def]
    intro U hU
    rw [WithGeneratedByTopology.isOpen_iff] at hU ⊢
    intro i f
    refine hU ⟨WithGeneratedByTopology.equiv.symm ∘ f, ?_⟩
    rw [continuous_iff X]
    intro j g
    rw [Function.comp_assoc, equiv_symm_comp_continuous_iff]
    fun_prop

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
this : ∅ ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Tactic:
rw [empty_union] at this

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C
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
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Tactic:
suffices eval (π C J) l = 0 by
    rw [this]
    exact Submodule.zero_mem _

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ eval (π C J) l = 0
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
this : ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = ↑E
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E

Tactic:
rw [empty_union] at this

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
this : ⋃ n, ⋃ j, openCell n ↑j = ↑E
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E
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

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:
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
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
inst✝ : CWComplex E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
by
    rw [empty_union]
    exact union

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
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
this : ord I (↑↑l).head! ≤ o
⊢ term I ho ≤ (↑↑l).head!

Tactic:
exact Products.rel_head!_of_mem hm

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
⊢ (⋂ i, s i).Nonempty

Tactic:
have h₂ : ⋂ i, s i = ⋂ i, s' i := by ext; simp; grind

Goal state after:
case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
⊢ (⋂ i, s i).Nonempty
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 ∧ SwapTrue o (↑x) i ≠ true
⊢ False

Tactic:
rw [← hi' i hi.1] at hi

Goal state after:
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
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
obtain ⟨x, hx⟩ := exist_norm_eq h

Goal state after:
case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
x : α
hx : ‖f x‖ = ‖f‖
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔ IsCountablyCompact univ

Tactic:
Subtype.isCountablyCompact_iff,

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔ IsCountablyCompact (Subtype.val '' univ)
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ ∀ s ∈ 𝓝 a, {a | x a ∈ s}.Infinite

Tactic:
exact fun s hs ↦ Infinite.of_accPt (hacc.nhds_inter hs) |>.mono (by grind) |>.of_image x

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : ↑x ≤ b
⊢ ((F i).concat (G i)) x ∈ U

Tactic:
rw [concat_left hfg hxb]
    refine hf ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
    simp [projIccCM, projIcc, hxb, x.2.1]

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
⊢ ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ∪ B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i

Tactic:
intro U hUo hAU

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst✝] (U i)
hAU : A ∪ B ⊆ ⋃ i, U i
⊢ ∃ t, t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.ContinuousMap.Sigma

Goal state before:
pp: X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
⊢ Function.Injective fun g ↦ (sigmaMk g.fst).comp g.snd

Tactic:
by
    rintro ⟨i, g⟩ ⟨i', g'⟩ h
    obtain ⟨rfl, hg⟩ : i = i' ∧ ⇑g ≍ ⇑g' :=
      Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h
    simpa using hg

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
y : N → ↑I
x✝ : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ y (e (e.symm n)) = 0 ∨ y (e (e.symm n)) = 1

Tactic:
by simpa using hn

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

Goal state before:
pp: case refine_2
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
⊢ J.Nonempty

Tactic:
← Finset.nonempty_coe_sort

Goal state after:
case refine_2
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
⊢ Nonempty ↥J
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
⊢ coveringNumber ε ∅ = 0

Tactic:
simp [coveringNumber]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ coveringNumber ε A = 0 ↔ A = ∅

Tactic:
simp [coveringNumber]

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∞ := ⋯
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 α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
this : ∀ (l : ℕ) (z : ↥(s (n + l))), ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
⊢ ↑((fun k ↦ Nat.recOn k ⟨x, hx⟩ fun l z ↦ ⋯.choose) 0) = x ∧
    ∀ (k : ℕ),
      edist ↑((fun k ↦ Nat.recOn k ⟨x, hx⟩ fun l z ↦ ⋯.choose) k)
          ↑((fun k ↦ Nat.recOn k ⟨x, hx⟩ fun l z ↦ ⋯.choose) (k + 1)) ≤
        B n / 2 ^ k

Tactic:
simp only [Nat.add_zero, Nat.rec_zero, true_and]

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' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
this : ∀ (l : ℕ) (z : ↥(s (n + l))), ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
⊢ ∀ (k : ℕ), edist ↑(Nat.rec ⟨x, hx⟩ (fun l z ↦ ⋯.choose) k) ↑⋯.choose ≤ B n / 2 ^ k
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : Compacts α
h : edist s t = 0
⊢ ↑s = ↑t

Tactic:
by
    have : closure (s : Set α) = closure t := hausdorffEDist_zero_iff_closure_eq_closure.1 h
    rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
⊢ ↑s = ↑t

Tactic:
by
    have : closure (s : Set α) = closure t := hausdorffEDist_zero_iff_closure_eq_closure.1 h
    rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
exact (not_nontrivial_iff.mp hs).infsep_zero

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ ediam (⇑toSnowflaking '' s) = ediam s ^ α

Tactic:
by
  simp [image_toSnowflaking_eq_preimage]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
x✝ : α
⊢ x✝ ∈ nhdsKer s ↔ x✝ ∈ ↑(upperClosure s)

Tactic:
simp [mem_nhdsKer_iff_specializes, specializes_iff_le]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
x✝ : α
⊢ x✝ ∈ nhdsKer s ↔ x✝ ∈ ↑(lowerClosure s)

Tactic:
simp [mem_nhdsKer_iff_specializes, specializes_iff_le]

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, IsOpen α t
⊢ IsOpen α (⋃₀ s)

Tactic:
simp only [IsOpen] at hs ⊢
  convert! CompleteLattice.ωScottContinuous.sSup hs
  aesop

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

Goal state before:
pp: X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
J : ↑q = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ hausdorffDist (range Subtype.val) ↑q

Tactic:
J

Goal state after:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
J : ↑q = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ hausdorffDist (range Subtype.val) (range Subtype.val)
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.{w, v} C
inst✝ : HasTerminal C
A : C
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
⊢ p₀ ∈ unop U

Tactic:
simpa using i.unop.le h

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

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
h✝ : p₀ ∈ U
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

Tactic:
cat_disch

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

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
h✝ : p₀ ∉ U
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

Tactic:
cat_disch

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

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens ↑X
h : p₀ ∈ U
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (map' p₀ f ≫ map' p₀ g).app (op U)

Tactic:
cat_disch

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

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens ↑X
h : p₀ ∉ U
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (map' p₀ f ≫ map' p₀ g).app (op U)

Tactic:
cat_disch

Goal state after: