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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates

Tactic:
apply coinduct fun {basis} ms =>
    ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), (motive (h_basis ▸ ms))
  · rintro basis ms (h_ms | ⟨rfl, h_ms⟩)
    · cases h_ms <;> grind
    simp only [reduceCtorEq, List.cons.injEq, ↓existsAndEq, and_true, heq_eq_eq, ms_eq_mk_iff,
      true_and, exists_eq_right_right', exists_and_left, false_or] at h_ms ⊢
    rcases h_step _ h_ms with h_step | ⟨exp, coef, tl, h_seq, h_coef, h_maj, h_tl⟩
    · grind
    · refine .inr ⟨basis_hd, ms.toFun, basis_tl, exp, coef, by simpa, ‹_›, tl, ?_⟩
      simp
      grind
  · grind

Goal state after:
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
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ^ q ∈ {x | x ≠ 0}

Tactic:
simp [hf0]

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

Goal state before:
pp: n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
this : k < m
⊢ False

Tactic:
have : m < k + 1 := lt_of_pow_lt_pow_left' d h_right

Goal state after:
n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
this✝ : k < m
this : m < k + 1
⊢ False
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n
⊢ ∀ (n n' : ℕ), n' = (b :: as₁).length + n → ∀ (bs : List Prop), mk ((b :: as₁).reverseAux bs) n' ↔ mk bs n

Tactic:
| cons b as₁ ih =>

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inr.mp
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
⊢ Tendsto F ℱ (𝓝 f)

pp: case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
· exact UniformFun.uniformContinuous_toFun.continuous.tendsto _ |>.comp H

Goal state after:
case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
⊢ ProfiniteCompletion.lift (𝟙 G ≫ ProfiniteCompletion.eta G) = 𝟙 (ProfiniteCompletion.completion G)

Tactic:
by
    apply ProfiniteCompletion.lift_unique
    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.lift ((f ≫ g) ≫ ProfiniteCompletion.eta Z✝) =
    ProfiniteCompletion.lift (f ≫ ProfiniteCompletion.eta Y✝) ≫
      ProfiniteCompletion.lift (g ≫ ProfiniteCompletion.eta Z✝)

Tactic:
by
    apply ProfiniteCompletion.lift_unique
    cat_disch

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
f : WithConv (E →L[R] F)
⊢ IsSelfAdjoint f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

Tactic:
simp [IsSelfAdjoint, WithConv.ext_iff, ContinuousLinearMap.ext_iff, star_eq_iff_star_eq,
    eq_comm (a := f _)]

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case h₁
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, f x_1 ∈ {f x}ᶜ

Tactic:
simpa [hf2.eq_iff] using! eventually_mem_nhdsWithin

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

Goal state before:
pp: case mp
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
⊢ X.str F ∈ S

Tactic:
by_contra c

Goal state after:
case mp
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
⊢ False
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mpr.inl
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h1 : S ∈ F → X.str F ∈ S
h2 : X.str F ∈ Sᶜ
h : S ∈ F
⊢ Sᶜ ∈ F

pp: case mpr.inr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h1 : S ∈ F → X.str F ∈ S
h2 : X.str F ∈ Sᶜ
h : Sᶜ ∈ F
⊢ Sᶜ ∈ F

Tactic:
exacts [absurd (h1 h) h2, h]

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

Goal state before:
pp: 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
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
⊢ P ∈ C2 → P.Nonempty

Tactic:
hP

Goal state after:
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
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
⊢ P.Nonempty
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: 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
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
P : Set (Ultrafilter X.A)
⊢ P ∈ C2 → P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q

Tactic:
hP

Goal state after:
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
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
P : Set (Ultrafilter X.A)
hP : P ∈ C2
⊢ P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case nil
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
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) [] →
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) []).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ []})

Tactic:
intro _

Goal state after:
case nil
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✝ : List.IsChain (fun x1 x2 ↦ x1 > x2) []
⊢ (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) []).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ []})
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
⊢ ∀ {x y : X.A} (f : Ultrafilter X.A), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y

Tactic:
intro _

Goal state after:
X : Compactum
x✝ : X.A
⊢ ∀ {y : X.A} (f : Ultrafilter X.A), ↑f ≤ 𝓝 x✝ → ↑f ≤ 𝓝 y → x✝ = y
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
P : Ultrafilter X
⊢ P ∈ Ultrafilter.lim ⁻¹' U → P ∈ {G | U ∈ G}

Tactic:
hP

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
P : Ultrafilter X
hP : P ∈ Ultrafilter.lim ⁻¹' U
⊢ P ∈ {G | U ∈ G}
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: ⊢ ∀ {X Y : Compactum}, Function.Injective compactumToCompHaus.map

Tactic:
intro _

Goal state after:
X✝ : Compactum
⊢ ∀ {Y : Compactum}, Function.Injective compactumToCompHaus.map
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: D : CompHaus
x✝ : Set (Compactum.ofTopologicalSpace ↑D.toTop).A
h1 : IsOpen x✝
⊢ ∀ (F : Ultrafilter ↑D.1), F.lim ∈ id ⁻¹' x✝ → id ⁻¹' x✝ ∈ ↑F

Tactic:
intro _

Goal state after:
D : CompHaus
x✝ : Set (Compactum.ofTopologicalSpace ↑D.toTop).A
h1 : IsOpen x✝
F✝ : Ultrafilter ↑D.1
⊢ F✝.lim ∈ id ⁻¹' x✝ → id ⁻¹' x✝ ∈ ↑F✝
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: D : CompHaus
x✝ : Set (Compactum.ofTopologicalSpace ↑D.toTop).A
h1 : IsOpen x✝
⊢ ∀ (F : Ultrafilter ↑D.1), F.lim ∈ id ⁻¹' x✝ → id ⁻¹' x✝ ∈ ↑F

Tactic:
intro _ h2

Goal state after:
D : CompHaus
x✝ : Set (Compactum.ofTopologicalSpace ↑D.toTop).A
h1 : IsOpen x✝
F✝ : Ultrafilter ↑D.1
h2 : F✝.lim ∈ id ⁻¹' x✝
⊢ id ⁻¹' x✝ ∈ ↑F✝
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
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed {f | f (term I ho) = false}

Tactic:
have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h : Continuous fun f ↦ f (term I ho)
⊢ IsClosed {f | f (term I ho) = false}
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
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed {f | f (term I ho) = true}

Tactic:
have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h : Continuous fun f ↦ f (term I ho)
⊢ IsClosed {f | f (term I ho) = true}
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : List I
hl : List.IsChain (fun x1 x2 ↦ x1 > x2) l
hll : Products.isGood {fun x ↦ false} ⟨l, hl⟩
⊢ ¬List.Lex (fun x1 x2 ↦ x1 < x2) [] l

Tactic:
intro _

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : List I
hl : List.IsChain (fun x1 x2 ↦ x1 > x2) l
hll : Products.isGood {fun x ↦ false} ⟨l, hl⟩
a✝ : List.Lex (fun x1 x2 ↦ x1 < x2) [] l
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (⇑((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)) ∘ ProjRestrict C fun x ↦ ord I x < o₂) =
    ⇑((πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))

Tactic:
← LocallyConstant.toFun_eq_coe,

Goal state after:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)).toFun ∘ ProjRestrict C fun x ↦ ord I x < o₂) =
    ⇑((πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndependent ℤ (eval C)

Tactic:
rw [linearIndependent_iff_union_smaller C ho hsC, linearIndependent_subtype_iff]

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndepOn ℤ id (⋃ e, smaller C ↑e)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent ℤ (eval C)

Tactic:
linearIndependent_iff_sum C hsC ho'

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent ℤ (SumEval C ho')
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case neg
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
j : cell C n
h : j ∉ I n
⊢ Disjoint D (openCell n j) ∧ ∀ (i : ℕ) (i_1 : ↑(I i)), Disjoint (openCell i ↑i_1) (openCell n j)

Tactic:
exact ⟨disjointBase n j |>.symm, fun _ _ ↦ disjoint_openCell_of_ne (by aesop)⟩

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
⊢ f ∈ comp Subtype.val M '' F ⁻¹' A

Tactic:
rw [show f = F g by ext; rfl] at hf ⊢

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
hf : F g ∈ A
⊢ F g ∈ comp Subtype.val M '' F ⁻¹' A
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
hA : IsSeqCompact A
x : ℕ → F
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
⊢ Tendsto (x ∘ φ) atTop (𝓝 (f a))

Tactic:
suffices f ∘ y ∘ φ = x ∘ φ from this ▸ (hf.continuous.tendsto a).comp hφ.2

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
hA : IsSeqCompact A
x : ℕ → F
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
⊢ f ∘ y ∘ φ = x ∘ φ
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 ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f) (⋃₀ s) (⋃₀ t)

Tactic:
have : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo f L (⋃₀ t) := by
        intro x hx
        rcases hKT hx with ⟨V, hVt, hxV⟩
        rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
        exact ⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩
      choose! L hLS hLmem hLt using this
      rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, hs⟩
      refine ⟨L '' s, image_subset_iff.2 fun x hx ↦ hLS x <| hsK x hx, s.finite_toSet.image _,
        by rwa [sUnion_image], ?_⟩
      rw [mapsTo_sUnion, forall_mem_image]
      exact fun x hx ↦ hLt x <| hsK x hx

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

Goal state before:
pp: case h.refine_1
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
⊢ ∀ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, IsCompact K_1

Tactic:
simp only [mem_iUnion, mem_range]

Goal state after:
case h.refine_1
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
⊢ ∀ (K_1 : Set X), (∃ i y, Subtype.val '' (K i) y = K_1) → IsCompact K_1
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ 𝓝 ⊤ = ⊤

Tactic:
by simp [nhds_eq]

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

Goal state before:
pp: θ : ↑I
⊢ 2 * ↑(0, θ).1 / (1 + ↑(0, θ).2) ≤ 0

Tactic:
by simp only [coe_zero, mul_zero, zero_div, le_refl]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace ↑V
v₀ : ↑V
hid : (ContinuousMap.id ↑V).Homotopic (ContinuousMap.const (↑V) v₀)
⊢ (ContinuousMap.inclusion hVU).Nullhomotopic

Tactic:
refine ⟨ContinuousMap.inclusion hVU v₀, ?_⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace ↑V
v₀ : ↑V
hid : (ContinuousMap.id ↑V).Homotopic (ContinuousMap.const (↑V) v₀)
⊢ (ContinuousMap.inclusion hVU).Homotopic (ContinuousMap.const (↑V) ((ContinuousMap.inclusion hVU) v₀))
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: ⊢ ¬(𝓝 ∞).IsCountablyGenerated

Tactic:
by
  intro
  have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance
  rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this
  exact not_countably_generated_cocompact this

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

Goal state before:
pp: y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y

Tactic:
have := ofDigits_cantorToTernary (ofDigits_bool_to_fin_three_mem_cantorSet y)

Goal state after:
y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
⊢ (fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩)
      ((fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }) p) =
    p

Tactic:
ext y; exact congr_arg p (eq_const_of_unique y).symm

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
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ ↔
    (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂)

Tactic:
constructor <;> rintro ⟨H⟩
    · exact
        ⟨{  toFun := fun tx ↦ H (tx.fst, fun _ ↦ tx.snd)
            map_zero_left := fun _ ↦ H.apply_zero _
            map_one_left := fun _ ↦ H.apply_one _
            prop' := fun t y iH ↦ H.prop' _ _ ⟨default, iH⟩ }⟩
    refine
      ⟨⟨⟨⟨fun tx ↦ H (tx.fst, tx.snd default), H.continuous.comp ?_⟩, fun y ↦ ?_, fun y ↦ ?_⟩, ?_⟩⟩
    · fun_prop
    · exact (H.apply_zero _).trans (congr_arg a₁ (eq_const_of_unique y).symm)
    · exact (H.apply_one _).trans (congr_arg a₂ (eq_const_of_unique y).symm)
    · rintro t y ⟨i, iH⟩
      cases Unique.eq_default i
      exact (H.eq_fst _ iH).trans (congr_arg a₁ (eq_const_of_unique y).symm)

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + (edist (x, s) (y, t) + edist (x, s) (y, t)) = infEDist y ↑t + 2 * edist (x, s) (y, t)

Tactic:
by rw [← mul_two, mul_comm]

Goal state after: