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

Goal state before:
pp: o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
by
  rcases e₁ : split o₁ with ⟨a, m⟩
  obtain ⟨N₁, r₁⟩ := nf_repr_split e₁
  obtain - | ⟨a0, n, a'⟩ := a
  #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
  The next block was previously
  ```
  · rcases m with - | m
    · by_cases h : o₂ = 0
      · simp [opow_def, opowAux2, e₁, h, r₁]
      · simpa [opow_def, opowAux2, e₁, h, r₁, eqComm] using mt repr_inj.1 h
    · rcases e₂ : split' o₂ with ⟨b', k⟩
      obtain ⟨_, r₂⟩ := nf_repr_split' e₂
      by_cases h : m = 0
      · simp [opowAux2, opow_def, e₁, h, r₁, r₂]
      simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
          Nat.cast_succ, _root_.zero_add,
          add_zero]
  ```
  The replacement proof is a short-term fix, and we request that the authors/maintainers of
  this file review the proof, and either approve it by removing this note, revise
  the proof or the prerequisites appropriately, or minimize a problem in lean4 that still
  needs addressing. -/
  · rcases m with - | m
    · have hzero : (0 : ONote) = zero := rfl
      by_cases h : o₂ = 0
      · subst h; simp [-zero_def, opow_def, opowAux2, e₁, r₁, hzero]
      · have h' := mt repr_inj.1 h
        have hne : o₂ ≠ zero := fun he => h (he ▸ rfl)
        simp [-zero_def, opow_def, opowAux2, e₁, r₁, hne, hzero]
        exact (zero_opow h').symm
    · rcases e₂ : split' o₂ with ⟨b', k⟩
      obtain ⟨_, r₂⟩ := nf_repr_split' e₂
      by_cases h : m = 0
      · simp only [opowAux2, opow_def, e₁, h, r₁, r₂, OfNat.ofNat, Zero.zero, One.one,
          repr]
        simp [opow_add, opow_mul]
      simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
          Nat.cast_succ, _root_.zero_add, add_zero]
      rw [opow_add, opow_mul, opow_omega0]
      · simp
      · simpa [Nat.one_le_iff_ne_zero]
      · rw [← Nat.cast_succ, lt_omega0]
        exact ⟨_, rfl⟩
  · have := N₁.fst
    have := N₁.snd
    obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)
    have al := split_add_lt e₁
    have aa : repr (a' + ofNat m) = repr a' + m := by
      simp only [ONote.repr_ofNat, ONote.repr_add]
    rcases e₂ : split' o₂ with ⟨b', k⟩
    obtain ⟨_, r₂⟩ := nf_repr_split' e₂
    simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]
    rcases k with - | k
    · simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc]
    · simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc, repr_one]
      rw [repr_opow_aux₁ a00 al aa, scale_opowAux]
      simp only [repr_mul, repr_scale, repr_one,
        Nat.cast_one, opow_one, opow_mul]
      rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]
      congr 1
      rw [← pow_succ, ← opow_natCast, ← opow_natCast]
      exact (repr_opow_aux₂ _ ad a00 al _ _).2

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

Goal state before:
pp: case h.cons.some
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
v : α × Subtype FriendlyOperation
hF : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2 s.tail)) (some v)
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match some v with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))

Tactic:
obtain ⟨hd, opf', op'⟩ := v
  simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at hF
  simp only [hF, Option.map_map]
  rw [hT]
  rfl

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

Goal state before:
pp: case oadd.inl.some
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.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)

Tactic:
refine ⟨?_, fun H ↦ H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩

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.oadd m b).repr = succ (a.oadd m b').repr

case oadd.inl.some.refine_2
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')
H : (a.oadd m b).NF
⊢ b'.repr < ω ^ a.repr
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A).getD 0 = 0
⊢ ⟨a, (List.dlookup a A).getD 0⟩ ∈ A.dedupKeys ∧ (decide ¬(List.dlookup a A).getD 0 = 0) = true

Tactic:
rw [← List.dlookup_dedupKeys] at h ⊢

Goal state after:
case h
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
⊢ ⟨a, (List.dlookup a A.dedupKeys).getD 0⟩ ∈ A.dedupKeys ∧ (decide ¬(List.dlookup a A.dedupKeys).getD 0 = 0) = true
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
hS4 : S4 = (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
replace hS4 : IsClosed S4 :=
    hS4.symm ▸ (isClosed_set_pi (fun _ _ ↦ hWc.isClosed)).inter (MonoidHom.isClosed_range_coe X Y)

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 : IsClosed[Pi.topologicalSpace] S4
⊢ LocallyCompactSpace (X →ₜ* Y)
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior (g • V • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty

Tactic:
interior_smul

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (g • interior (V • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty
Module: Mathlib.Topology.Algebra.ProperAction.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : Torsor V P
inst✝² : TopologicalSpace V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
Φ : V × P ≃ₜ P × P :=
  { toFun := fun vp ↦ (vp.1 • vp.2, vp.2), invFun := fun pq ↦ (pq.1 /ₛ pq.2, pq.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
exact Φ.isProperMap

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

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
⊢ ∀ {x : Circle}, x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)

Tactic:
x

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
⊢ x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)
Module: Mathlib.Topology.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
f : R → R × R := fun u ↦ (star u * u, u * star u)
u : R
⊢ u ∈ f ⁻¹' {(1, 1)} ↔ u ∈ ↑(unitary R)

Tactic:
simp [f, Unitary.mem_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Valued R (WithZero (Multiplicative ℤ))
x : R
hx : v x ≤ exp (-1)
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0)

Tactic:
by
  refine tendsto_zero_pow_of_v_lt_one (hx.trans_lt ?_)
  rw [← exp_zero, exp_lt_exp]
  simp

Goal state after:
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
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
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)
⊢ IsClosed[inst✝] A

Tactic:
← inter_eq_left.2 asubc

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
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
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)
⊢ IsClosed[inst✝] (A ∩ C)
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
⊢ ⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {↑a (op J)} ⊇ ⇑(π_app C fun x ↦ x ∈ K) ⁻¹' {↑a (op K)}

Tactic:
x

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
⊢ x ∈ ⇑(π_app C fun x ↦ x ∈ K) ⁻¹' {↑a (op K)} → x ∈ ⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {↑a (op J)}
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
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
⊢ Disjoint (openCell n i) (D ∪ ⋃ n, ⋃ j, openCell n ↑j)

Tactic:
simp_rw [disjoint_union_right, disjoint_iUnion_right]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
⊢ Disjoint (openCell n i) D ∧ ∀ (i_1 : ℕ) (i_2 : ↑(J i_1)), Disjoint (openCell n i) (openCell i_1 ↑i_2)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
⊢ T2Space X.A

Tactic:
rw [t2_iff_ultrafilter]

Goal state after:
X : Compactum
⊢ ∀ {x y : X.A} (f : Ultrafilter X.A), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = 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 : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Tactic:
have h' := Products.prop_of_isGood_of_contained C _ h hsC

Goal state after:
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 : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i < Order.succ o
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ ∀ (n_1 : ℕ) (i : ↑{x | ↑n_1 < n}), closedCell n_1 ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
by
      intro l ⟨i, hi⟩
      apply subset_union_of_subset_right
      apply subset_iUnion₂_of_subset l hi
      exact subset_iUnion _ _

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ m + 1 ≤ n + 1

Tactic:
by gcongr

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
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
⊢ MapsTo (⇑((F i).concat (G i))) K U

Tactic:
x

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
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
⊢ x ∈ K → ((F i).concat (G i)) x ∈ U
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS : ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
⊢ ∀ (x : X), ∀ V ∈ countableBasis Y, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V

Tactic:
x

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS : ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
x : X
⊢ ∀ V ∈ countableBasis Y, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case refine_3
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds continuousAt_snd

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 ∈ ⇑f ⁻¹' V, ∃ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, K_1 ∈ 𝓝 x ∧ MapsTo (⇑f) K_1 V

Tactic:
x

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
⊢ 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.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⋂ s ∈ l, {x | s ∈ x} = {x | x ≤ l}

Tactic:
← ofPred_forall,

Goal state after:
α : Type u_2
l : Filter α
⊢ {x | ∀ i ∈ l, i ∈ x} = {x | x ≤ l}
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
x : Option α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball x r)

Tactic:
match x with
    | (x : α) =>
      obtain ⟨s', s'o, s's⟩ := m.topology_eq_on_restrict x r
      refine ⟨some '' s', ?_, ?_⟩
      · exact (IsOpenEmbedding.isOpen_iff_image_isOpen h).mp s'o
      ext ⟨y, yh⟩
      match y with
      | none => contradiction
      | (z : α) =>
        apply Set.ext_iff.mp at s's
        simp only [mem_preimage, Subtype.forall, Metric.mem_eball, mem_image] at s's ⊢ yh
        specialize s's z yh
        refine ⟨fun ⟨r, rh, rh'⟩ ↦ ?_, fun _ ↦ ⟨z, by tauto⟩⟩
        exact s's.1 <| h.injective rh' ▸ rh
    | none =>
      apply discreteTopology_iff_forall_isOpen.mp
      rw [ball_infty_of_pos ENNReal.zero_lt_top]
      exact Subsingleton.discreteTopology

Goal state after: