mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
⊢ ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → (∀ x ∈ tl.head, hd > x) ∧ motive tl

Tactic:
intro (exp, coef) tl h
      constructor
      · intro (tl_exp, tl_coef) h_tl
        rw [gt_iff_lt, lt_iff_lt]
        replace h_step := (h_step exp coef tl h).right.left
        cases tl <;> simp [leadingExp, head] at h_tl h_step
        grind
      · grind [h_step exp coef tl h]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ dist s t = 0

Tactic:
by
    apply eq_of_le_of_ge
    · apply ge_of_tendsto' (x := Filter.atTop) _ this
      rw [tendsto_pow_atTop_nhds_zero_iff]
      norm_num
    · simp

Goal state after:
Module: Mathlib.Tactic.NormNum.NatSqrt

Goal state before:
pp: x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ x.sqrt = y

Tactic:
by
  rw [← hr, ← pow_two]
  rw [two_mul] at hle
  exact Nat.sqrt_add_eq' _ (Nat.le_of_ble_eq_true hle)

Goal state after:
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h' : n = 0
⊢ IsSquare a

Tactic:
simp [h.1, h']

Goal state after:
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h' : n = 0
⊢ IsSquare a

Tactic:
simp [h.1, h']

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case pos
a d : ℕ
q : ℚ
hq : 0 ≤ q
h_coprime : a.Coprime 0
ha : ↑a / ↑0 = q ^ d
⊢ ∃ x, a = x ^ d

Tactic:
simp only [Nat.coprime_zero_right] at h_coprime

Goal state after:
case pos
a d : ℕ
q : ℚ
hq : 0 ≤ q
ha : ↑a / ↑0 = q ^ d
h_coprime : a = 1
⊢ ∃ x, a = x ^ d
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
by_cases hq : 0 ≤ q
  · apply not_power_rat_of_num_aux h_coprime ha hq
  rcases d.even_or_odd with (h_even | h_odd)
  · have := not_power_rat_of_num_aux h_coprime (q := -q) ha (by linarith)
    rwa [h_even.neg_pow] at this
  · contrapose hq
    rw [← h_odd.pow_nonneg_iff, ← hq]
    positivity

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
⊢ Irrational (x ^ y)

Tactic:
have hy_den_pos : 0 < y_den := by
    by_contra! h
    simp only [nonpos_iff_eq_zero] at h
    simp only [h, pow_zero, Nat.lt_one_iff] at hn1 hn2
    lia
  rcases hx_isNNRat with ⟨hx_inv, hx_eq⟩
  rcases hy_isNNRat with ⟨hy_inv, hy_eq⟩
  rw [hy_eq, hx_eq]
  have h1 : (y_num * ⅟(y_den : ℝ) : ℝ) = ((y_num / y_den : ℚ) : ℝ) := by
    simp
    rfl
  have h2 : (x_num * ⅟(x_den : ℝ) : ℝ) = ((x_num / x_den : ℚ) : ℝ) := by
    simp
    rfl
  rw [h1, h2]
  refine irrational_rpow_rat_of_not_power ?_ hy_den_pos ?_
  · simp only [div_pow, ← Nat.cast_pow]
    apply not_power_rat_of_num
    · apply Nat.Coprime.pow _ _ hx_coprime
    · apply not_power_nat_pow_of_bounds hy_den_pos hy_coprime hn1 hn2
  · positivity

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

Goal state before:
pp: case some.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h₃ : (if x' = x then some y else dlookup x (map Prod.toSigma (xs.zip ys))) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
split_ifs at h₃ with h

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : some y = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

case neg
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: case mp
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✝ ∈ S4 → x✝ ∈ DFunLike.coe '' S1

Tactic:
rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩

Goal state after:
case mp
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) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
f : X →ₜ* Y
hf : f ∈ S2
⊢ ⇑↑f ∈ DFunLike.coe '' S1
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
⊢ ∃ V, Disjoint (a • ↑V) (b • ↑V)

Tactic:
obtain ⟨u, v, _, open_v, mem_u, mem_v, dis⟩ := t2_separation (h ∘ inv_mul_eq_one.mp)
  obtain ⟨V, hV⟩ := is_nonarchimedean v (open_v.mem_nhds mem_v)
  use V
  simp only [Disjoint, Set.bot_eq_empty, Set.subset_empty_iff]
  intro x mem_aV mem_bV
  by_contra! ⟨s, hs⟩
  have hsa : s ∈ a • (V : Set G) := mem_aV hs
  have hsb : s ∈ b • (V : Set G) := mem_bV hs
  rw [mem_leftCoset_iff] at hsa hsb
  refine dis.subset_compl_right mem_u (hV ?_)
  simpa [mul_assoc] using mul_mem hsa (inv_mem hsb)

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ Metric.sphere 0 1
y : EuclideanSpace ℝ (Fin n)
hy : y ∈ Metric.sphere 0 1
h :
  (ConcreteCategory.hom (diskBoundaryInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (diskBoundaryInclusion n)) { down := ⟨y, hy⟩ }
⊢ x = y

Tactic:
by simpa [diskBoundaryInclusion, disk] using h

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

Goal state before:
pp: case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this✝ : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ basic A ∧ X.str (X.join G) = X.str F

Tactic:
rw [join_distrib, this]

Goal state after:
case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this✝ : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ basic A ∧ X.str F = X.str F
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
⊢ ↑F ≤ 𝓝 x → X.str F = x

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `AA)
   []
   []
   ":="
   (Set.«term_⁻¹'_»
    `X.str
    "⁻¹'"
    (choice
     («term{_}» "{" [`x] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
      (Term.optEllipsis [])
      []
      "}"))))))

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
⊢ ↑F ≤ 𝓝 x → X.str F = x
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
⊢ ∀ (n : ℕ) (i : CWComplex.cell C n),
    ∃ I,
      MapsTo (↑(CWComplex.map n i)) (sphere 0 1)
        (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(CWComplex.map m j) '' closedBall 0 1)

Tactic:
simpa only [empty_union] using CWComplex.mapsTo'

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
I J : (n : ℕ) → Set (cell C n)
hIJ : ⋃ n, ⋃ j, openCell n ↑j = ⋃ n, ⋃ j, openCell n ↑j
⊢ I = J

Tactic:
apply RelCWComplex.eq_of_eq_union_iUnion
  simp_rw [empty_union, hIJ]

Goal state after:
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
h' : o ≤ ord I i
hsC : g i = true
⊢ g i = true ∧ Order.succ o ≤ ord I i

Tactic:
exact ⟨hsC, Order.succ_le_of_lt (h'.lt_of_ne' 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
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (eval C)) ↔ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))

Tactic:
refine ⟨fun h ↦ le_trans h (span_mono (fun a ⟨b, hb⟩ ↦ ⟨b.val, hb⟩)), fun h ↦ le_trans 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))
⊢ Submodule.span ℤ (Set.range (Products.eval C)) ≤ Submodule.span ℤ (Set.range (eval C))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos.hnc
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 ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ¬↑x (term I ho) = true

Tactic:
simp [mem_C'_eq_false C ho x x.prop]

Goal state after:
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
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 ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ¬∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 0

Tactic:
push Not at h₂; obtain ⟨i, hi⟩ := h₂; exfalso; rw [hi' i hi.1] at hi; exact hi.2 (h₁ i hi.1)

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

Goal state before:
pp: α : 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
⊢ MapsTo (⇑(G i)) K₂ U → (F i) ⊤ = (G i) ⊥ → MapsTo (⇑((F i).concat (G i))) K U

Tactic:
hg

Goal state after:
α : 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
⊢ (F i) ⊤ = (G i) ⊥ → MapsTo (⇑((F i).concat (G i))) K U
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
⊢ ∃ a ∈ A, AccPt a (𝓟 B)

Tactic:
let f := hB.natEmbedding
  let x : ℕ → E := (↑) ∘ f
  have hx_inj : Function.Injective x := Subtype.val_injective.comp f.injective
  obtain ⟨a, haA, hac⟩ :=
    IsCountablyCompact.seq_clusterPt hA x (Eventually.of_forall (fun n => hBA (f n).2))
  refine ⟨a, haA, accPt_iff_clusterPt.2 <| ClusterPt.mono hac <| le_inf ?_ ?_⟩
  · exact tendsto_principal.mpr <| Nat.cofinite_eq_atTop ▸
      ((Set.finite_singleton a).preimage hx_inj.injOn).compl_mem_cofinite
  · exact tendsto_principal.mpr <| Eventually.of_forall fun n => (f n).2

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

Goal state before:
pp: 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
hVo : IsOpen[inst✝³] V
x : X
⊢ x ∈ ⇑f ⁻¹' V → ∃ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, K_1 ∈ 𝓝 x ∧ MapsTo (⇑f) K_1 V

Tactic:
hxV

Goal state after:
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
hVo : IsOpen[inst✝³] V
x : X
hxV : 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.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ (fun x ↦ x ∈ { carrier := u, is_open' := h }) ⁻¹' {True} = u

Tactic:
by simp [Set.preimage]

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

Goal state before:
pp: G G' : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : Group G'
inst✝ : IsTopologicalGroup G'
⊢ hSpace (G × G') = HSpace.prod G G'

Tactic:
simp only [HSpace.prod]
  rfl

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
⊢ (match (x, y) with
    | (x, y) =>
      match (Ux, Uy) with
      | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
    ContractibleSpace
      ↑(match (Ux, Uy) with
        | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
⟨hUx, hUy⟩

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy
⊢ ContractibleSpace
    ↑(match (Ux, Uy) with
      | (Ux, Uy) => Ux ×ˢ Uy)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case hba
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
refine Set.not_subset.mpr ⟨(logSizeBallSeq J hJ a c i).point, ?_, ?_⟩

Goal state after:
case hba.refine_1
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ ↑(logSizeBallSeq J hJ a c i).finset

case hba.refine_2
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∉ ↑(logSizeBallSeq J hJ a c (i + 1)).finset
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case h
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ (logSizeBallSeq J hJ a c j).smallBall c ⊆ ?u

Tactic:
exact (Finset.filter_subset _ _).trans (antitone_logSizeBallSeq_add_one_subset hJ h)

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

Goal state before:
pp: N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : (t₀ = 0 ∨ t₀ = 1) ∨ t ∈ boundary { j // j ≠ i }
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
obtain H | ⟨j, H⟩ := H

Goal state after:
case inl
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

case inr
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ ((homotopyTo i✝ H) t) y = x

Tactic:
rw [homotopyTo_apply, H.eq_fst, p.2]

Goal state after:
case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N

case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ i ∈ Finset.range (n1 + 1), ofDigitsTerm a i + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ i ∈ Finset.range (n1 + 1), ofDigitsTerm b i + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False

Tactic:
Finset.sum_range_succ,

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ x ∈ Finset.range n1, ofDigitsTerm a x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ i ∈ Finset.range (n1 + 1), ofDigitsTerm b i + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ x ∈ Finset.range n1, ofDigitsTerm a x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ i ∈ Finset.range (n1 + 1), ofDigitsTerm b i + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False

Tactic:
Finset.sum_range_succ,

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ x ∈ Finset.range n1, ofDigitsTerm a x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm b n1 + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False