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

Goal state before:
pp: case single_add.inl
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e'
a✝ : single e' y + f = f → eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
⊢ eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)

pp: case single_add.inr
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
a✝ : single e' y + f = f → eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
he' : e' < e
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)

Tactic:
· simp only [← add_assoc, ← single_add, eval_single_add' _ hf, mul_add]

Goal state after:
case single_add.inr
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
a✝ : single e' y + f = f → eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
he' : e' < e
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ = a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
subst IHa

Goal state after:
case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
h✝¹ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝¹).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
h✝ : o₂ = e₁.oadd n₂ a₁
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₁) h✝).NF
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₁) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ DecidableRel TopBelow

Tactic:
intro b o
  cases o <;> delta TopBelow <;> infer_instance

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ f ⟦x✝¹⟧ ∈ image f ⟦PSet.mk α✝ A✝⟧

Tactic:
by
    simp only [mk_eq, ← Definable₁.mk_out (f := f)]
    exact ⟨a, Definable₁.out_equiv f ya⟩

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

Goal state before:
pp: case eq.zero
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
· by_cases en : n₁ = n₂
        · simpa [en]
        · simp only [en, ite_false]
          exact
            (Ordinal.sub_eq_zero_iff_le.2 <|
                le_of_lt <|
                  oadd_lt_oadd_2 h₁ <|
                    lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm

Goal state after:
case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊆ x✝.toZFSet ∧ ¬x✝.toZFSet ⊆ x✝¹.toZFSet

Tactic:
simp [h, h.le]

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

Goal state before:
pp: o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)

Goal state after:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ a.repr + ↑m < ω ^ e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
⊢ (o₁ ^ o₂).NF

Tactic:
by_cases h : o₂ = 0

Goal state after:
case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : o₂ = 0
⊢ (o₁ ^ o₂).NF

case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : ¬m = 0
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, *]
        change NF (oadd _ _ 0)
        infer_instance

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
⊢ Majorized (f ^ exp) f exp

Tactic:
simp only [Majorized]
  intro exp' h_exp
  apply (isLittleO_iff_tendsto' _).mpr
  · have : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ (f t) ^ (exp - exp') :=
      (h.eventually_gt_atTop 0).mono (fun _ h ↦ by simp [← Real.rpow_sub h])
    apply Tendsto.congr' this.symm
    conv =>
      arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp h
  · apply (Tendsto.eventually_gt_atTop h 0).mono
    intro t h1 h2
    absurd h2
    exact (Real.rpow_pos_of_pos h1 _).ne.symm

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

Goal state before:
pp: α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst✝ : DecidablePred P
⊢ ∀ (s t : Stream'.Seq α), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t

Tactic:
intro s t

Goal state after:
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst✝ : DecidablePred P
s t : Stream'.Seq α
⊢ dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
by_cases h : o₂ = 0

Goal state after:
case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
⊢ ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t

Tactic:
intro s t

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
⊢ dist (op s) (op t) ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)

Tactic:
have h_eq : UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =
                    UnitMonomial.toFun exps_tl basis_tl := by
          ext x; simp [UnitMonomial.toFun, h.left]
        rw [h_eq]
        exact toFun_tendsto_zero_of_firstNonzeroIsNeg h_basis.tail (by simpa using h_length) h.right

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

Goal state before:
pp: case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
h_step : leadingExp tl < ↑exp
⊢ tl_exp < exp

Tactic:
cases tl <;> simp [leadingExp, head] at h_tl h_step

Goal state after:
case step.left.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x✝ : ℝ × MultiseriesExpansion basis_tl
s✝ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x✝ s✝))
h_tl : x✝ = (tl_exp, tl_coef)
h_step : x✝.1 < exp
⊢ tl_exp < exp
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF

Tactic:
· refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))
        rw [repr, repr_zero, add_zero, iha.1, opow_succ]
        gcongr
        apply natCast_lt_omega0

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

Goal state before:
pp: a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : 2 ∣ 1
⊢ False

Tactic:
← even_iff_two_dvd

Goal state after:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : Even 1
⊢ False
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: en enl ea eal : Q(ℕ)
ehn : Q(IsNat «$en» «$enl»)
eha : Q(IsNat «$ea» «$eal»)
n : ℕ := Expr.natLit! enl
__x✝¹ : PLift (0 < n)
hn0 : 0 < n
a : ℕ := Expr.natLit! eal
b : ℕ := n.minFac
__x✝ : PLift (a ≤ b)
hab : a ≤ b
h_bn : b < n
m : ℕ := n / b
em : Q(ℕ)
ehm : Q(IsNat (OfNat.ofNat «$em») «$em»)
h_ba_eq : b = a
⊢ a * m = n

Tactic:
by simp [m, b, ← h_ba_eq, Nat.mul_div_cancel' (minFac_dvd _)]

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

Goal state before:
pp: 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⟩ ∈ U
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
rw [← hsv, Set.mem_preimage] at uDefaultSpec

Goal state after:
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
⊢ (U ∩ Set.range (etaFn G)).Nonempty
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
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
J : (g'⁻¹ • V) • {x} ∈ 𝓝 x
⊢ U • {x} ∈ 𝓝 x

Tactic:
have : (g'⁻¹ • V) • {x} ⊆ U • ({x} : Set X) := by
    apply smul_subset_smul_right
    apply Subset.trans (smul_set_subset_smul (inv_mem_inv.2 hg')) ?_
    rw [V_symm]
    exact VU

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 : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
J : (g'⁻¹ • V) • {x} ∈ 𝓝 x
this : (g'⁻¹ • V) • {x} ⊆ U • {x}
⊢ U • {x} ∈ 𝓝 x
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
⊢ a ∈ A

Tactic:
by_contra! nh

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
⊢ False
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
h : i ∉ E.I n
⊢ Disjoint (openCell n i) (D ∪ ⋃ n, ⋃ j, openCell n ↑j)

Tactic:
disjoint_union_right,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
h : i ∉ E.I n
⊢ Disjoint (openCell n i) D ∧ Disjoint (openCell n i) (⋃ n, ⋃ j, openCell n ↑j)
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:
by
  rw [generatedBy, instTopologicalSpaceSigma, coinduced_iSup, iSup_sigma]
  rfl

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

Goal state before:
pp: case mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic A ∩ basic B → G ∈ basic (A ∩ B)

Tactic:
· rintro ⟨h1, h2⟩
    exact inter_mem h1 h2

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: case refine_1
ι : 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 b : (fun X ↦ ↑X.toTop) (indexCone hC).pt
h :
  (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a =
    (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) b
J : Finset ι
⊢ (π_app C fun x ↦ x ∈ J) a = (π_app C fun x ↦ x ∈ J) b

Tactic:
apply_fun fun f : (limitCone.{u, u} (indexFunctor hC)).pt => f.val (op J) at h

Goal state after:
case refine_1
ι : 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 b : (fun X ↦ ↑X.toTop) (indexCone hC).pt
J : Finset ι
h :
  ↑((ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a) (op J) =
    ↑((ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) b) (op J)
⊢ (π_app C fun x ↦ x ∈ J) a = (π_app C fun x ↦ x ∈ J) b
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:
disjoint_union_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 ∧ Disjoint (openCell n i) (⋃ n, ⋃ j, openCell n ↑j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
h : contained C o
this : (∀ (i : I), ∀ x ∈ C, x i = true → ord I i < o) → (Proj fun x ↦ ord I x < o) '' C = C
⊢ C = π C fun x ↦ ord I x < o

Tactic:
exact (this (fun i x hx ↦ h x hx i)).symm

Goal state after:
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
⊢ LinearIndepOn ℤ id (⋃ e, smaller C ↑e)

Tactic:
exact linearIndepOn_iUnion_of_directed
    (Monotone.directed_le fun _ _ h ↦ GoodProducts.smaller_mono C h) fun ⟨o', ho'⟩ ↦
    (linearIndependent_iff_smaller _ _).mp (h o' ho' (ho'.le.trans hho)
    (π C (ord I · < o')) (isClosed_proj _ _ hC) (contained_proj _ _))

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

Goal state before:
pp: case pos
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
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

Tactic:
rw [h, max_eq_o_cons_tail C hsC ho l]

Goal state after:
case pos
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
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) [] (term I ho :: ↑(↑l).Tail)
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 : x ∈ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ s

Tactic:
match x with
    | none =>
      exact ⟨1, by norm_num, by simpa [ball_infty_of_pos]⟩
    | (x : α) =>
      obtain ⟨ε, εp, εt⟩ := (@EMetric.isOpen_iff α (PseudoEMetricSpace.ofEDist edist
        m.edist_self m.edist_comm m.edist_triangle)).mp
          (m.topology_le _ <| h.continuous.isOpen_preimage s so) x (mem_preimage.mpr xs)
      exact ⟨ε, εp, some_eball x ε ▸ image_subset_iff.mpr εt⟩

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
⊢ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑g

Tactic:
by
  rw [eventually_nhdsSet_iff_forall] at *
  intro x hx
  apply ((hf x hx).and (h x hx).eventually_nhds).mono
  intro y hy
  convert! hy.1 using 1
  exact Germ.coe_eq.mpr hy.2

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

Goal state before:
pp: case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ pairSetSeq J a c i ⊆ J ×ˢ J

Tactic:
simp only [pairSetSeq, hJ, ↓reduceDIte]
    apply Finset.product_subset_product
    · exact Finset.singleton_subset_iff.mpr (point_mem_logSizeBallSeq_init hJ _)
    exact (Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)

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
f : ↑(Ω^ N X x)
g : (N → ↑I) → X
h : g = ⇑f
⊢ copy f g h = f

Tactic:
by
  ext x
  exact congr_fun h x

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

Goal state before:
pp: case inl
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hM : y ∘ Sum.inl ∈ Cube.boundary M
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

pp: case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
· have : p (y ∘ Sum.inl) = const := p.property (y ∘ Sum.inl) hM
    simp [this]

Goal state after:
case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x
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
i : N
p : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (Cube.insertAt i) (((Cube.splitAt i) y✝).1, ((Cube.splitAt i) y✝).2) = y✝

Tactic:
exact Equiv.apply_symm_apply _ _

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

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
| 1

Tactic:
← one_pow n

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
| 1 ^ n
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:

Tactic:
infEDist x s ≤ infEDist x t + hausdorffEDist (t : Set α) s :=
      infEDist_le_infEDist_add_hausdorffEDist
    _ ≤ infEDist y t + edist x y + hausdorffEDist (t : Set α) s := by
      gcongr; apply infEDist_le_infEDist_add_edist
    _ = infEDist y t + (edist x y + hausdorffEDist (s : Set α) t) := by
      rw [add_assoc, hausdorffEDist_comm]
    _ ≤ infEDist y t + (edist (x, s) (y, t) + edist (x, s) (y, t)) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = infEDist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]

Goal state after: