mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o a x : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a = ω ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
by
  refine ⟨?_, fun ⟨hx, ha⟩ ↦ ?_⟩
  · obtain rfl | ho := eq_zero_or_pos o
    · rw [veblen_zero] at h
      have := invVeblen₁_of_lt_opow h
      have := invVeblen₂_of_lt_opow h
      aesop
    · rw [← veblen_veblen_of_lt ho, veblen_zero_apply, opow_right_inj one_lt_omega0]
      rintro rfl
      simp [invVeblen₁_veblen h, invVeblen₂_veblen ho.ne' h]
  · convert! ← veblen_invVeblen₁_invVeblen₂ x

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank

Tactic:
apply max_le <;> apply rank_mono <;> intro _ h

Goal state after:
case a.h₁
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ x
⊢ x✝ ∈ x ∪ y

case h₂
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ y
⊢ x✝ ∈ x ∪ y
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x
A : Class.{u}
x : ZFSet.{u}
right✝ : A x
⊢ Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x

Tactic:
exact H x

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
h : x.IsOrdinal
⊢ ∀ {a b : ↥x},
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a b ∨ a = b ∨ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b a

Tactic:
intro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
x : ZFSet.{u}
h : x.IsOrdinal
a : ZFSet.{u}
ha : a ∈ x
b : ZFSet.{u}
hb : b ∈ x
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) ⟨a, ha⟩ ⟨b, hb⟩ ∨
    ⟨a, ha⟩ = ⟨b, hb⟩ ∨ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) ⟨b, hb⟩ ⟨a, ha⟩
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ a.toZFSet ∈ b.toZFSet

Tactic:
by
  rw [mem_toZFSet_iff]
  exact ⟨a, h, rfl⟩

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
r t : R
h : -r = t
⊢ -(algebraMap R A) r = (algebraMap R A) t

Tactic:
by
  rw [← map_neg, h]

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

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
t : ℝ
hx : 0 < b t
⊢ b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp

Tactic:
conv_rhs => rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]

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

Goal state before:
pp: α : Type u_1
s t : Stream' α
⊢ dist s t ≤ 1

Tactic:
by_cases h : s = t
  · simp [h]
  rw [PiNat.dist_eq_of_ne h]
  bound

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

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
h_basis : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf : ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis [f]

Tactic:
by simpa [WellFormedBasis]

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

Goal state before:
pp: α : Type u_1
hd : α
⊢ FriendlyOperation (Seq.cons hd)

Tactic:
simp only [friendlyOperation_iff_dist_le_dist, dist_cons_cons]
  intro x y
  linarith [dist_nonneg (x := x) (y := y)]

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

Goal state before:
pp: case cons.succ
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
m : Fin basis_tl.length
⊢ (mk (Multiseries.cons 0 (monomialRpow basis_tl (↑m) r) Multiseries.nil) (basis_tl[↑m] ^ r)).Approximates

Tactic:
apply (monomialRpow_approximates h_basis.tail).cons _ (by simp)

Goal state after:
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
m : Fin basis_tl.length
⊢ Majorized (basis_tl[↑m] ^ r) basis_hd 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Multiseries.nil.Trimmed

Tactic:
by
  constructor

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.some.refine_1
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ ω ^ a.repr * ↑↑m + b.repr = succ (a.oadd m b').repr

Tactic:
ihb.1,

Goal state after:
case oadd.inl.some.refine_1
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ ω ^ a.repr * ↑↑m + succ b'.repr = succ (a.oadd m b').repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
exact this

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
exact this

Goal state after:
case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
exact this

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

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

Tactic:
subst h_coprime

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

Goal state before:
pp: num denom : ℕ
inv : Invertible ↑denom
⊢ √(↑(Int.negOfNat num) * ⅟↑denom) = ↑0

Tactic:
have h₁ : 0 ≤ (num : ℚ) * ⅟(denom : ℝ) :=
    mul_nonneg (Nat.cast_nonneg' _) (invOf_nonneg.2 <| Nat.cast_nonneg' _)

Goal state after:
num denom : ℕ
inv : Invertible ↑denom
h₁ : 0 ≤ ↑↑num * ⅟↑denom
⊢ √(↑(Int.negOfNat num) * ⅟↑denom) = ↑0
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
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)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
have ind : IsInducing (UniformFun.ofFun ∘ (↑) : S → X →ᵤ α) :=
      hS.inducing_uniformFun_iff_pi.mpr ⟨rfl⟩

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)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ Set.range toContinuousMap = {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}

Tactic:
refine Set.Subset.antisymm (Set.range_subset_iff.2 fun f ↦ ⟨map_one f, map_mul f⟩) ?_

Goal state after:
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y} ⊆ Set.range toContinuousMap
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: 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
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
have hS4 : S4 = (↑) '' S1 := by
    ext
    constructor
    · rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩
      exact ⟨f, hf, rfl⟩
    · rintro ⟨f, hf, rfl⟩
      exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩

Goal state after:
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
hS4 : S4 = DFunLike.coe '' S1
⊢ LocallyCompactSpace (X →ₜ* Y)
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: 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 Subtype.val
hS4 : S4 = DFunLike.coe '' S1
⊢ Equicontinuous Subtype.val

Tactic:
rwa [← hS4] at h

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

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this✝ :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
this :
  (Hom.hom (((Functor.const (OpenNormalSubgroup ↑P.toProfinite.toTop)).obj P.cone.pt).map g ≫ P.cone.π.app Y))
      ((ConcreteCategory.hom f) t) =
    (Hom.hom (P.cone.π.app X ≫ P.diagram.map g)) ((ConcreteCategory.hom f) t)
⊢ (ConcreteCategory.hom (quotientMap f Y))
      ((ConcreteCategory.hom
          ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
        ↑t) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) ↑t)

Tactic:
exact this

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:
norm_pow,

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
⊢ ‖c‖ ^ (k + 1) ≤ 1
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
⊢ C = D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1

Tactic:
← union',

Goal state after:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
⊢ D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
S : Set X.A
⊢ IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
← isOpen_compl_iff

Goal state after:
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
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
⊢ generatedBy X = coinduced (fun x ↦ x.fst.snd x.snd) inferInstance

Tactic:
generatedBy,

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance = coinduced (fun x ↦ x.fst.snd x.snd) inferInstance
Module: Mathlib.Topology.CWComplex.Classical.Basic

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

Tactic:
exact this

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:
exact this

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
⊢ x ∈ π (π C K) J ↔ x ∈ π C J

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π (π C K) J
⊢ x ∈ π C J

case refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π C J
⊢ x ∈ π (π C K) J
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
x : ↑(π C J)
⊢ (fun i ↦ ↑x ↑i) ∈ IndexFunctor.obj C J

Tactic:
rcases x with ⟨x, y, hy, rfl⟩

Goal state after:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
y : I → Bool
hy : y ∈ C
⊢ (fun i ↦ ↑⟨Proj J y, ⋯⟩ ↑i) ∈ IndexFunctor.obj C J
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
i : I
⊢ IsLocallyConstant fun f ↦ if ↑f i = true then 1 else 0

Tactic:
by
    rw [IsLocallyConstant.iff_continuous]
    exact (continuous_of_discreteTopology (f := fun (a : Bool) ↦ (if a then (1 : ℤ) else 0))).comp
      ((continuous_apply i).comp continuous_subtype_val)

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

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

Tactic:
by
    intro _ _ _ _ h
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` gets confused by coercion using forget.
    apply Monad.Algebra.Hom.ext
    ext
    simpa using! ConcreteCategory.congr_hom h _

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
⊢ ord I i = o ↔ term I ho = i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : ord I i = o
⊢ term I ho = i

case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o
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:
exact this

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : Products I
⊢ Products.isGood C l ↔ Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
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

case refine_2
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 fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
⊢ Products.isGood C l
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
| f ⁻¹' {y}

Tactic:
← Set.univ_inter (f ⁻¹' {y}),

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
| Set.univ ∩ f ⁻¹' {y}
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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
· have := l.val.prop
    rw [max_eq_o_cons_tail C hsC ho l, List.isChain_iff_pairwise] at this
    exact List.rel_of_pairwise_cons this (List.head!_mem_self hM)

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

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∈ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∉ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

Tactic:
· exact isMaxOn_iff.mp hmax x hx

Goal state after:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∉ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
this : ¬SeqCompactSpace E
⊢ False

Tactic:
simp only [seqCompactSpace_iff, IsSeqCompact, mem_univ, not_forall,
    true_and, not_exists, not_and, exists_const] at this

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
this : ∃ x, ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
⊢ False