mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (rename (Prod.mk 0)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) *
      (rename (Prod.mk 1)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            (rename (Prod.mk 1)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          (rename (Prod.mk 0)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) +
      remainder p n

Tactic:
map_sum,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
      (rename (Prod.mk 1)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            (rename (Prod.mk 1)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
⊢ y ∈ pullSub T x → ∃ z ∈ T, y = x ++ z

Tactic:
intro ⟨h1, h2⟩

Goal state after:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ ∃ z ∈ T, y = x ++ z
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case neg
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
constructor <;> intro ⟨h, _⟩

Goal state after:
case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take x.length z <+: x
right✝ : List.drop x.length z ∈ pullSub T y
⊢ z ∈ pullSub T (x ++ y)

case neg.mpr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take (x ++ y).length z <+: x ++ y
right✝ : List.drop (x ++ y).length z ∈ T
⊢ z ∈ pullSub (pullSub T y) x
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
b✝ : Bool
a0 : Lists' α b✝
l0 l₂ : Lists' α true
s : a0.cons' l0 ⊆ l₂
h : a ∈ (a0.cons' l0).toList
⊢ a ∈ l₂

Tactic:
obtain - | ⟨e, m, s⟩ := s
    simp only [toList, Sigma.eta, List.mem_cons] at h
    rcases h with (rfl | h)
    · exact ⟨_, m, e⟩
    · exact mem_of_subset' s h

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ∈ Set.range (lfpApprox f ⊥)

Tactic:
use ord <| succ #α
  exact lfpApprox_ord_eq_lfp f

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝²] {a}

Tactic:
obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff.1 ha

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
⊢ IsOpen[inst✝²] {a}
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ ∀ a ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2,
    ∀ (b_1 : Ordinal.{u_1}), b ^ a * ((single e x) a + f a) + b_1 = b ^ a * f a + b_1

Tactic:
intro e'

Goal state after:
case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
⊢ (e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2) →
    ∀ (b_1 : Ordinal.{u_1}), b ^ e' * ((single e x) e' + f e') + b_1 = b ^ e' * f e' + b_1
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' ≤ e
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
cases f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e' y f hf hy =>
    obtain rfl | he' := (h e' (by simp [hy])).eq_or_lt
    · simp only [← add_assoc, ← single_add, eval_single_add' _ hf, mul_add]
    · rw [eval_single_add']
      refine fun a ha ↦ (h a ha).lt_of_ne ?_
      rintro rfl
      apply (hf a _).not_gt he'
      simpa [he'.ne'] using ha

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

Goal state before:
pp: o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ veblenWith f o = derivFamily fun x ↦ veblenWith f ↑x

Tactic:
rw [veblenWith, if_neg h]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ (∀ (i : ↑(Iio o)), veblenWith f (↑i) a = a) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
exact Subtype.forall

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ (∃ z, z = x ∧ y ∈ z) ↔ y ∈ x

Tactic:
exists_eq_left

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

Goal state before:
pp: x : ZFSet.{u}
h : x.Nonempty
⊢ ↑(⋂₀ x) = ⋂₀ (SetLike.coe '' ↑x)

Tactic:
ext
  simp [mem_sInter h]

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

Goal state before:
pp: x y : ZFSet.{u}
hxy : x ⊆ y
⊢ x ∩ y = x

Tactic:
ext; simpa using @hxy _

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
| ((e₁.oadd n₁ a₁).sub (e₂.oadd n₂ a₂)).repr

Tactic:
dsimp only [sub]

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
| (match e₁.cmp e₂ with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match ↑n₁ - ↑n₂ with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁).repr
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ n • b + -1 • b = (n + -1) • b

Tactic:
← add_zsmul

Goal state after:
G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ (n + -1) • b = (n + -1) • b
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ y ⊆ x

Tactic:
exact mem_or_subset hx hy

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

Goal state before:
pp: o : Ordinal.{u}
a : ↑(Set.Iio o)
⊢ ↑a < o

Tactic:
decreasing_by exact a.2

Goal state after:
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ -1 • b + n • b = (-1 + n) • b

Tactic:
← add_zsmul

Goal state after:
G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ (-1 + n) • b = (-1 + n) • b
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
b : G
h : -b = -1 • b
⊢ -1 • b + -1 • b = -2 • b

Tactic:
← add_zsmul

Goal state after:
G : Type u_1
inst✝ : AddGroup G
b : G
h : -b = -1 • b
⊢ (-1 + -1) • b = -2 • b
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
h : IsSuccPrelimit o
z : ZFSet.{u}
⊢ z ∈ V_ o ↔ z ∈ ⋃ (a : ↑(Set.Iio o)), V_ ↑a

Tactic:
by simpa [mem_vonNeumann] using h.lt_iff_exists_lt

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

Goal state before:
pp: x : ZFSet.{u_1}
h : x.IsOrdinal
⊢ (insert x x).IsOrdinal

Tactic:
by
  refine ⟨fun y hy ↦ ?_, @fun y z w hyz hzw hw ↦ ?_⟩
  · obtain rfl | hy := mem_insert_iff.1 hy
    on_goal 2 => apply (h.subset_of_mem hy).trans
    all_goals simp_all [subset_def]
  · obtain rfl | hw := mem_insert_iff.1 hw
    exacts [h.mem_trans hyz hzw, h.mem_trans' hyz hzw hw]

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

Goal state before:
pp: case zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ (e.opowAux a0 a 0 0).repr = ω ^ e.repr * (opowAux 0 a0 a 0 0).repr

Tactic:
simp [opowAux]

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

Goal state before:
pp: case succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
n✝ : ℕ
⊢ (e.opowAux a0 a 0 (n✝ + 1)).repr = ω ^ e.repr * (opowAux 0 a0 a 0 (n✝ + 1)).repr

Tactic:
simp [opowAux]

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

Goal state before:
pp: α : Type u_1
s : Stream'.Seq α
⊢ FriendlyOperation fun x ↦ s

Tactic:
simp [friendlyOperation_iff_dist_le_dist]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
              (T s.head)
⊢ FriendlyOperation op

Tactic:
refine Seq.FriendlyOperation.coind_comp_friend_left motive h_base (fun op h_op ↦ ?_)
  obtain ⟨T, hT⟩ := h_step op h_op
  use fun hd? ↦ (T hd?).map (fun (exp, coef, opf, op') => ((exp, coef), opf, op'))
  intro s
  rw [destruct_eq_destruct_map, hT s]
  simp
  rfl

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
⊢ (ms.replaceFun f).Approximates

Tactic:
by
  let motive (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : Prop :=
      ∃ (ms' : MultiseriesExpansion (basis_hd :: basis_tl)) (f' : ℝ → ℝ),
      ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
  apply Approximates.coind motive ⟨ms, f, by grind⟩
  rintro _ ⟨ms, f, rfl, h_approx, h_eq⟩
  cases ms with
  | nil g =>
    simp only [nil_iff, mk_toFun, mk_replaceFun, mk_seq, true_and,
      Multiseries.nil_ne_cons, false_and, exists_const, or_false] at h_approx h_eq ⊢
    grw [← h_eq, h_approx]
  | cons exp coef tl g =>
    obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
    refine .inr ⟨exp, coef, tl, ?_⟩
    simp only [mk_replaceFun, mk_seq, h_coef, mk_toFun, true_and]
    simp only [mk_toFun] at h_eq
    refine ⟨h_maj.of_eventuallyEq h_eq.symm, mk tl (g - basis_hd ^ exp * coef.toFun), _, rfl,
      h_tl, ?_⟩
    grw [mk_toFun, h_eq]

Goal state after:
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a = b
H : a' - b' - (a - b) = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Goal state after:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ a' - b' = 0
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: 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
⊢ Irrational (x ^ (↑y_num * ⅟↑y_den))

Tactic:
hx_eq

Goal state after:
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
⊢ Irrational ((↑x_num * ⅟↑x_den) ^ (↑y_num * ⅟↑y_den))
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y

Tactic:
cases ys
      · cases h₁
      · obtain - | ⟨h₀, h₁⟩ := h₀
        simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
        rw [if_neg]
        · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
        · apply h₀; apply List.mem_of_getElem? h₂

Goal state after:
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 → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
rw [isInducing_iff, isInducing_iff]
  change (_ = ((UniformOnFun.uniformSpace X α 𝔖).comap F).toTopologicalSpace) ↔
    (_ = ((Pi.uniformSpace _).comap ((⋃₀ 𝔖).domRestrict ∘ F)).toTopologicalSpace)
  rw [← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]

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

Goal state before:
pp: case h
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
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : ↑origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((diagram G).map M_to_Na)) (spc m) ∈ fJ a

Tactic:
exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).right

Goal state after:
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
⊢ V • V ⊆ U

Tactic:
exact VU

Goal state after:
Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ SequentialSpace X

Tactic:
by
  rw [← IsGeneratedBy.generatedBy_eq (X := fun n ↦ Fin n → ℝ) (Y := X)]
  exact SequentialSpace.iSup (fun n ↦ SequentialSpace.iSup
    (fun f ↦ SequentialSpace.coinduced _))

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✝ : 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
⊢ False

Tactic:
have h' : Disjoint (openCell n i) (D ∪ ⋃ n, ⋃ (j : J n), openCell (C := C) n j) := by
    simp_rw [disjoint_union_right, disjoint_iUnion_right]
    exact ⟨disjointBase n i, fun m j ↦ disjoint_openCell_of_ne (by lia)⟩

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
h' : Disjoint (openCell n i) (D ∪ ⋃ n, ⋃ j, openCell n ↑j)
⊢ False
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
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply subset_iUnion₂_of_subset m hm

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ ⋃ j, closedCell m j
Module: Mathlib.Topology.Category.Compactum

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

Tactic:
by
        apply mem_of_superset this
        intro P hP
        exact c2 U P hP hU

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x
c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst✝²] U → {G | U ∈ G} ∈ FF
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact c4

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

Goal state before:
pp: case hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
hn : ∀ m ≤ n, ∀ (i : cell C m), ∃ I, cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ I m_1, openCell m_1 j
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n.succ i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell m j
⊢ ∃ I, cellFrontier (n + 1) i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell m j

Tactic:
choose p hp using hn

Goal state after:
case hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n.succ i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell m j
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
⊢ ∃ I, cellFrontier (n + 1) i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x✝ : ↑(ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ))
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho))) x✝ = (ModuleCat.Hom.hom 0) x✝

Tactic:
apply CC_comp_zero

Goal state after:
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
⊢ Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

Tactic:
· left
      intro he
      apply h
      have h' := Products.prop_of_isGood_of_contained C _ h hsC
      simp only [Order.lt_succ_iff] at h'
      have hh' : ∀ a ∈ l.val, ord I a < o := by
        intro a ha
        refine (h' a ha).lt_of_ne ?_
        rw [ne_eq, ord_term ho a]
        rintro rfl
        contradiction
      rwa [Products.eval_πs_image C hh', ← Products.eval_πs C hh',
        Submodule.apply_mem_span_image_iff_mem_span (injective_πs _ _)]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
⊢ IsCompactSystem S

Tactic:
intro C hC

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ ⋂ i, C i = ∅ → ∃ n, dissipate C n = ∅
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ∀
    ⦃x :
      (n : ℕ) ×
        match n with
        | 0 => ↑D
        | n.succ => PEmpty.{u_1 + 1}⦄,
    x ∈ univ →
      ∀
        ⦃y :
          (n : ℕ) ×
            match n with
            | 0 => ↑D
            | n.succ => PEmpty.{u_1 + 1}⦄,
        y ∈ univ →
          x ≠ y →
            (Disjoint on fun ni ↦
                (fun a ↦
                    ↑(match ni.fst, ni.snd with
                        | 0, i => PartialEquiv.single ![] ↑i
                        | n.succ, i => i.elim)
                      a) ''
                  ball 0 1)
              x y

Tactic:
Function.onFun

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ∀
    ⦃x :
      (n : ℕ) ×
        match n with
        | 0 => ↑D
        | n.succ => PEmpty.{u_1 + 1}⦄,
    x ∈ univ →
      ∀
        ⦃y :
          (n : ℕ) ×
            match n with
            | 0 => ↑D
            | n.succ => PEmpty.{u_1 + 1}⦄,
        y ∈ univ →
          x ≠ y →
            Disjoint
              ((fun a ↦
                  ↑(match x.fst, x.snd with
                      | 0, i => PartialEquiv.single ![] ↑i
                      | n.succ, i => i.elim)
                    a) ''
                ball 0 1)
              ((fun a ↦
                  ↑(match y.fst, y.snd with
                      | 0, i => PartialEquiv.single ![] ↑i
                      | n.succ, i => i.elim)
                    a) ''
                ball 0 1)