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

Goal state before:
pp: case cons.cons.cons
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
h1 : exps1.length = exps2.length
h2 : ∀ f ∈ basis_tl, 0 < f x
h3 : 0 < basis_hd x
⊢ basis_hd x ^ (exp1 + exp2) *
      (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 exps2) basis_tl).prod =
    basis_hd x ^ exp1 * (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis_tl).prod *
      (basis_hd x ^ exp2 * (List.zipWith (fun exp b ↦ b x ^ exp) exps2 basis_tl).prod)

Tactic:
rw [ih h_basis.tail h1 h2, Real.rpow_add h3]

Goal state after:
case cons.cons.cons
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
h1 : exps1.length = exps2.length
h2 : ∀ f ∈ basis_tl, 0 < f x
h3 : 0 < basis_hd x
⊢ basis_hd x ^ exp1 * basis_hd x ^ exp2 *
      ((List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis_tl).prod *
        (List.zipWith (fun exp b ↦ b x ^ exp) exps2 basis_tl).prod) =
    basis_hd x ^ exp1 * (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis_tl).prod *
      (basis_hd x ^ exp2 * (List.zipWith (fun exp b ↦ b x ^ exp) exps2 basis_tl).prod)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp1 exp2 : ℝ
coef1 coef2 : MultiseriesExpansion basis_tl
tl1 tl2 : Multiseries basis_hd basis_tl
⊢ Seq.cons (exp1, coef1) tl1 = Seq.cons (exp2, coef2) tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2

Tactic:
Seq.cons_eq_cons

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp1 exp2 : ℝ
coef1 coef2 : MultiseriesExpansion basis_tl
tl1 tl2 : Multiseries basis_hd basis_tl
⊢ (exp1, coef1) = (exp2, coef2) ∧ tl1 = tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop (𝓝 coef)

Tactic:
by
  intro t
  eta_expand
  simp only [toFun, Pi.smul_apply, smul_eq_mul]
  convert Filter.Tendsto.const_mul _ (UnitMonomial.toFun_tendsto_one_of_allZero h_exps)
  simp [t]

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

Goal state before:
pp: case succ
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
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'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
base : motive s t
⊢ dist s t ≤ 2⁻¹ ^ (n + 1)

Tactic:
obtain step | ⟨hd, u, v, c, rfl, rfl, h_next⟩ := step s t base

Goal state after:
case succ.inl
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
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'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
base : motive s t
step : s = t
⊢ dist s t ≤ 2⁻¹ ^ (n + 1)

case succ.inr
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
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'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
hd : α
u v : Stream'.Seq α
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ dist (Seq.cons hd (op c u)) (Seq.cons hd (op c v)) ≤ 2⁻¹ ^ (n + 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : g =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ (mk tl (g - basis_hd ^ exp * coef.toFun)).toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun

Tactic:
grw [mk_toFun, h_eq]

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

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
⊢ n ^ p ≠ m ^ q

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simpa [hq.ne'] using h 0
  contrapose! h
  let f := n.factorization.mapRange (· / q) <| by simp
  suffices hf : n.factorization = q • f by
    have hf0 : f 0 = 0 := by simpa [hq.ne'] using congr($hf 0)
    refine ⟨f.prod (· ^ ·), Nat.factorization_inj hn (by simp [hf0]) ?_⟩
    rwa [Nat.factorization_pow, n.factorization_prod_pow_eq_self_of_le_factorization ?_]
    exact hf ▸ le_self_nsmul zero_le (by lia)
  ext z
  rw [Finsupp.smul_apply, smul_eq_mul, Finsupp.mapRange_apply, Nat.mul_div_cancel']
  simpa using h_coprime.symm.dvd_of_dvd_mul_left ⟨_, by simpa using congr(Nat.factorization $h z)⟩

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

Goal state before:
pp: n k p q : ℕ
hq : 0 < q
h_coprime : p.Coprime q
h_left : k ^ q < n
h_right : n < (k + 1) ^ q
m : ℕ
⊢ n ^ p ≠ m ^ q

Tactic:
by
  apply not_power_nat_pow h_coprime hq
  intro m
  apply not_power_nat_of_bounds h_left h_right

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

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

Tactic:
by_cases hb_zero : b = 0

Goal state after:
case pos
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : b = 0
⊢ ↑a / ↑b ≠ q ^ d

case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
⊢ ↑a / ↑b ≠ q ^ d
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m : ℕ
⊢ a ^ b * a ^ b * a % m = a ^ b * (a ^ b * a) % m

Tactic:
mul_assoc

Goal state after:
a b m : ℕ
⊢ a ^ b * (a ^ b * a) % m = a ^ b * (a ^ b * a) % m
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ (some val).getD x ∈ ys ↔ x ∈ xs

Tactic:
| some val =>

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

Goal state before:
pp: case h₀
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀.Nodup

Tactic:
rwa [← h₀, hxs, hperm.nodup_iff]

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

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
⊢ ↑(etaFn G origin) a ∈ fJ a

Tactic:
let M_to_Na : m ⟶ a := (iInf_le (fun (j : J) => (j.val.toSubgroup)) ⟨a, a_in_J⟩).hom

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ ↑(etaFn G origin) a ∈ fJ a
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext x
    exact lim_eq (pure_le_nhds _)

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
x : ↑C
⊢ (LocallyConstant.evalMonoidHom x) (List.map (e C) ↑l).prod = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Tactic:
map_list_prod

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg.h₁.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
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs ≤ a :: b :: bs

Tactic:
apply le_of_lt

Goal state after:
case neg.h₁.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 := ⋯
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs < a :: b :: bs
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
f : ↑(π (C1 C ho) fun x ↦ ord I x < o)
⊢ SwapTrue o ↑f ∈ C1 C ho

Tactic:
by
  obtain ⟨f, g, hg, rfl⟩ := f
  convert! hg
  dsimp +unfoldPartialApp [SwapTrue]
  ext i
  split_ifs with h
  · rw [ord_term ho] at h
    simpa only [← h] using hg.2.symm
  · 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.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E F : Subcomplex C
h : (fun E ↦ E.carrier) E = (fun E ↦ E.carrier) F
⊢ E = F

Tactic:
by
    obtain ⟨E, _, _, hE⟩ := E
    obtain ⟨F, _, _, hF⟩ := F
    congr
    apply eq_of_eq_union_iUnion
    rw [hE, hF]
    simpa using h

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

Goal state before:
pp: S : Profinite
⊢ IsClosedEmbedding (ι S)

Tactic:
apply Continuous.isClosedEmbedding

Goal state after:
case h
S : Profinite
⊢ Continuous (ι S)

case hf
S : Profinite
⊢ Function.Injective (ι S)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})ᶜ

Tactic:
convert! C.2

Goal state after:
S : Profinite
C : { C // IsClopen C }
⊢ ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})ᶜ = ↑C
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true})

Tactic:
convert! C.2

Goal state after:
S : Profinite
C : { C // IsClopen C }
⊢ (fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true} = ↑C
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
h : (openCell n j ∩ interior D).Nonempty
⊢ False

Tactic:
rcases h with ⟨x, xmemcell, xmemD⟩

Goal state after:
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
xmemcell : x ∈ openCell n j
xmemD : x ∈ interior D
⊢ False
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case a
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
⊢ compactOpen ≤ generateFrom (image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T})

Tactic:
apply_rules [generateFrom_anti, image2_subset_iff.mpr]
    intro K hK t ht
    exact mem_image2_of_mem (hS₁ K hK) (isOpen_sUnion fun _ h ↦ hT.isOpen <| ht.2 h)

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

Goal state before:
pp: case empty
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
f : ι → Set E
hf : ∀ i ∈ ∅, IsCountablyCompact (f i)
⊢ IsCountablyCompact (⋃ i ∈ ∅, f i)

Tactic:
| empty =>

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
s : Set ι
f : ι → Set E
hs : s.Finite
hf : ∀ i ∈ s, IsCountablyCompact (f i)
s' : Finset ι := hs.toFinset
h1 : ⋃ i ∈ s, f i = ⋃ i ∈ s', f i
⊢ IsCountablyCompact (⋃ i ∈ s, f i)

Tactic:
exact h1 ▸ Finset.isCountablyCompact_biUnion s' (fun i hi => hf i ((hs.mem_toFinset).mp hi))

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

Goal state before:
pp: case h.refine_2.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
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f ∘ Subtype.val) ((K U) n) V

Tactic:
exact fun y _ ↦ hUV y.2

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

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : none ∈ s
⊢ ∃ ε > 0, Metric.eball none ε ⊆ s

Tactic:
exact ⟨1, by norm_num, by simpa [ball_infty_of_pos]⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (eHmul (p.1, p.2.1), eHmul (p.1, p.2.2))
hG : Continuous G
⊢ ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y)))).HomotopyRel
    (ContinuousMap.id (X × Y)) {(e, e)}

Tactic:
use! ⟨G, hG⟩

Goal state after:
case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG }.toFun (0, x) =
      ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
        x

case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ?map_zero_left,
                    map_one_left := ?map_one_left }.toFun
                (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
hG : Continuous G
⊢ ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e)))).HomotopyRel
    (ContinuousMap.id (X × Y)) {(e, e)}

Tactic:
use! ⟨G, hG⟩

Goal state after:
case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG }.toFun (0, x) =
      ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
        x

case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ?map_zero_left,
                    map_one_left := ?map_one_left }.toFun
                (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
          x
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: a✝ : (𝓝 ∞).IsCountablyGenerated
this : (comap OnePoint.some (𝓝 ∞)).IsCountablyGenerated
⊢ False

Tactic:
rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this

Goal state after:
a✝ : (𝓝 ∞).IsCountablyGenerated
this : (cocompact ℚ).IsCountablyGenerated
⊢ False
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: p : ℚ
s : Set ℚ
⊢ TotallyDisconnectedSpace ℚ

Tactic:
clear p s
  refine ⟨fun s hsu hs x hx y hy => ?_⟩; clear hsu
  by_contra H : x ≠ y
  wlog hlt : x < y
  · apply this s hs y hy x hx H.symm <| H.lt_or_gt.resolve_left hlt
  rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩
  have := hs.image _ continuous_coe_real.continuousOn
  rw [isPreconnected_iff_ordConnected] at this
  have : z ∈ Rat.cast '' s :=
    this.out (mem_image_of_mem _ hx) (mem_image_of_mem _ hy) ⟨hxz.le, hzy.le⟩
  exact hz (image_subset_range _ _ this)

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

Goal state before:
pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j

Tactic:
refine Group.ext (EckmannHilton.mul (isUnital_auxGroup i) (isUnital_auxGroup j) ?_)

Goal state after:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ ∀ (a b c d : HomotopyGroup N X x), a * b * (c * d) = a * c * (b * d)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

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

Tactic:
by simp [hx]

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

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)|

Tactic:
← le_abs_self

Goal state after:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + (dist b (x n) - dist a (x n))
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case inl
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ ∃ f, Isometry f

Tactic:
use fun _ => 0; intro x; exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)

Goal state after: