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

Goal state before:
pp: case h₂
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := ⋯
R : Ordinal.{0} := ⋯
ω0 : Ordinal.{0} := ⋯
α' : Ordinal.{0} := ⋯
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0✝ : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
αd : ω ∣ α'
α0 : ¬IsMin α'
⊢ ω ^ (a0.repr * succ ↑k) ≤ ω0 ^ succ ↑k * ↑↑n

Tactic:
· have := mul_le_mul_right (one_le_iff_pos.2 <| Nat.cast_pos'.2 n.pos) (ω0 ^ succ (k : Ordinal))
      rw [opow_mul]
      simpa

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
h_head : s.head = t.head
⊢ (op s).head = (op t).head

Tactic:
simp only [head_eq_destruct, Option.map_eq_map, h.destruct_apply_eq_unfold, Option.map_map]
    at h_head ⊢
  simp [h_head]
  rfl

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
R : ℝ × MultiseriesExpansion basis_tl → ℝ × MultiseriesExpansion basis_tl → Prop
exp : ℝ
coef : MultiseriesExpansion basis_tl
⊢ Seq.Pairwise R (cons exp coef nil)

Tactic:
simp [cons, nil]

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

Goal state before:
pp: case oadd.inl.none.inl.none.zero
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ (a.oadd 1 b).repr = succ zero.repr ∧ ((a.oadd 1 b).NF → zero.NF)

Tactic:
simp only [repr, repr_zero, iha, ihb, opow_lt_opow_iff_right one_lt_omega0,
        add_lt_add_iff_left, add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Goal state after:
case oadd.inl.none.inl.none.zero
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ 1 = succ 0 ∧ ((oadd 0 1 0).NF → NF 0)
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
simp only [repr, repr_zero, iha, ihb, opow_lt_opow_iff_right one_lt_omega0,
        add_lt_add_iff_left, add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Goal state after:
case oadd.inl.none.inl.none.succ
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ 1 * ↑m' + 1 + 1 = succ (1 * ↑m' + 1) ∧ ((oadd 0 (m' + 1).succPNat 0).NF → (oadd 0 m'.succPNat 0).NF)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.zero
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')
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ i, a_1 < (a'.oadd i.succPNat zero).repr

Tactic:
simp only [repr, repr_zero, iha, ihb, opow_lt_opow_iff_right one_lt_omega0,
        add_lt_add_iff_left, add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Goal state after:
case oadd.inl.none.inl.some.zero
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')
e' : m.natPred = 0
⊢ IsSuccLimit (ω ^ a'.repr * ω) ∧
    (∀ (i : ℕ),
        0 < ω ^ a'.repr ∧
          ω ^ a'.repr * ↑i + ω ^ a'.repr < ω ^ a'.repr * ω ∧ ((a.oadd 1 0).NF → (a'.oadd i.succPNat 0).NF)) ∧
      ∀ a < ω ^ a'.repr * ω, ∃ i, a < ω ^ a'.repr * ↑i + ω ^ a'.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ
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
⊢ IsSuccLimit (a.oadd (m' + 1).succPNat b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd (m' + 1).succPNat b ∧
            ((a.oadd (m' + 1).succPNat b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd (m' + 1).succPNat b).repr, ∃ i, a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr

Tactic:
simp only [repr, repr_zero, iha, ihb, opow_lt_opow_iff_right one_lt_omega0,
        add_lt_add_iff_left, add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Goal state after:
case oadd.inl.none.inl.some.succ
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
⊢ IsSuccLimit (ω ^ a'.repr * ω * ↑m' + ω ^ a'.repr * ω + ω ^ a'.repr * ω) ∧
    (∀ (i : ℕ),
        0 < ω ^ a'.repr ∧
          ω ^ a'.repr * ↑i + ω ^ a'.repr < ω ^ a'.repr * ω ∧
            ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF)) ∧
      ∀ a < ω ^ a'.repr * ω * ↑m' + ω ^ a'.repr * ω + ω ^ a'.repr * ω,
        ∃ i, a < ω ^ a'.repr * ω * ↑m' + ω ^ a'.repr * ω + (ω ^ a'.repr * ↑i + ω ^ a'.repr)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ i, a_1 < ((f i).oadd 1 zero).repr

Tactic:
simp only [repr, repr_zero, iha, ihb, opow_lt_opow_iff_right one_lt_omega0,
        add_lt_add_iff_left, add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Goal state after:
case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ i, a_1 < ω ^ (f i).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd (m' + 1).succPNat b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd (m' + 1).succPNat b ∧
            ((a.oadd (m' + 1).succPNat b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd (m' + 1).succPNat b).repr, ∃ i, a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr

Tactic:
simp only [repr, repr_zero, iha, ihb, opow_lt_opow_iff_right one_lt_omega0,
        add_lt_add_iff_left, add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr, ∃ i, a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ (f i).repr
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: b n : ℕ
hl : n.blt b = true
⊢ Nat.log b n = 0

Tactic:
Nat.blt_eq

Goal state after:
b n : ℕ
hl : n < b
⊢ Nat.log b n = 0
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1

Tactic:
Nat.blt_eq

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℤ
n : ℕ
h : IsNat a n
⊢ IsSquare n ↔ IsSquare a

Tactic:
simp [h.1, Int.isSquare_natCast_iff]

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

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = b * x ^ d
⊢ (y ^ d).Coprime (x ^ d)

Tactic:
apply Nat.Coprime.pow_left

Goal state after:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = b * x ^ d
⊢ y.Coprime (x ^ d)
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case refine_1
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ ∀ (p : ℚ), ↑(x_num ^ y_num) / ↑(x_den ^ y_num) ≠ p ^ y_den

Tactic:
apply not_power_rat_of_num

Goal state after:
case refine_1.h_coprime
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ (x_num ^ y_num).Coprime (x_den ^ y_num)

case refine_1.ha
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ ∀ (x : ℕ), x_num ^ y_num ≠ x ^ y_den
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
have H2 : (Pi.uniformSpace _).comap ((⋃₀ 𝔖).domRestrict ∘ F) =
      ⨅ (K ∈ 𝔖), (Pi.uniformSpace _).comap (K.domRestrict ∘ F) := by
    simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
      UniformSpace.comap_iInf]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
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
⊢ U • {x} ∈ 𝓝 x

Tactic:
have I : (interior ((g • V) • {x})).Nonempty := by
    apply hi.mono
    apply interior_mono
    exact smul_subset_smul_right inter_subset_right

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
⊢ 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)
nh : a ∉ A
⊢ A = A \ {a}

Tactic:
simp [nh]

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : AccPt x (𝓟 (closure[inst✝¹] A))
⊢ AccPt x (𝓟 A)

Tactic:
AccPt,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : (𝓝[≠] x ⊓ 𝓟 (closure[inst✝¹] A)).NeBot
⊢ (𝓝[≠] x ⊓ 𝓟 A).NeBot
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
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
⊢ ⋂₀ ι T ∈ C2

Tactic:
apply claim4.finiteInter_mem T

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
C0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
C1 : ssu := ⋯
C2 : Set (Set (Ultrafilter X.A)) := ⋯
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
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
⊢ ↑T ⊆ finiteInterClosure C1
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
f : (m : ℕ) → Finset (cell C m)
h : cellFrontier 1 e ⊆ ⋃ m, ⋃ (_ : m < 1), ⋃ j ∈ f m, closedCell m j
⊢ ∃ x y, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y

Tactic:
simp only [RelCWComplex.cellFrontier_one_eq, image_pair, Order.lt_one_iff, iUnion_iUnion_eq_left,
    RelCWComplex.closedCell_zero_eq_singleton, pair_subset_iff, mem_iUnion, mem_singleton_iff,
    exists_prop] at h

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
f : (m : ℕ) → Finset (cell C m)
h : (∃ i ∈ f 0, ↑(map 1 e) (-1) = ↑(map 0 i) ![]) ∧ ∃ i ∈ f 0, ↑(map 1 e) 1 = ↑(map 0 i) ![]
⊢ ∃ x y, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s)))

Tactic:
refine le_trans (spanFinBasis.span C s) ?_

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ Submodule.span ℤ (Set.range (spanFinBasis C s)) ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s)))
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)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : ↑(π C L)
i : I
⊢ ↑((ProjRestricts C hJK ∘ ProjRestricts C hKL) x) i = ↑(ProjRestricts C ⋯ x) i

Tactic:
simp only [π, Proj, Function.comp_apply, ProjRestricts_coe]

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)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : ↑(π C L)
i : I
⊢ (if J i then if K i then ↑x i else false else false) = if J i then ↑x i else false
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:
rw [IsLocallyConstant.iff_continuous]

Goal state after:
I : Type u
C : Set (I → Bool)
i : I
⊢ Continuous fun f ↦ if ↑f i = true then 1 else 0
Module: Mathlib.Topology.Category.Compactum

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

Tactic:
ext FF
    change Ultrafilter (Ultrafilter X) at FF
    set x := (Ultrafilter.map Ultrafilter.lim FF).lim with c1
    have c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen U → U ∈ F := by
      intro U F h1 hU
      exact isOpen_iff_ultrafilter.mp hU _ h1 _ (Ultrafilter.le_nhds_lim _)
    have c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x := by
      rw [le_nhds_iff]
      intro U hx hU
      exact mem_coe.2 (c2 _ _ (by rwa [← c1]) hU)
    have c4 : ∀ U : Set X, x ∈ U → IsOpen U → { G : Ultrafilter X | U ∈ G } ∈ FF := by
      intro U hx hU
      suffices Ultrafilter.lim ⁻¹' U ∈ FF by
        apply mem_of_superset this
        intro P hP
        exact c2 U P hP hU
      exact @c3 U (IsOpen.mem_nhds hU hx)
    apply lim_eq
    rw [le_nhds_iff]
    exact c4

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

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

Tactic:
simp only [term, ord, Ordinal.enum_typein]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
x : X
⊢ x ∈ skeleton C n ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
RelCWComplex.mem_skeleton_iff,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
x : X
⊢ (x ∈ ∅ ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j) ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
obtain (hs | hs) := (tsupport g).eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : tsupport g = ∅
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C

case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C