mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)

Tactic:
rw [disjoint_sUnion_left]

Goal state after:
case refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ ∀ s_1 ∈ s, Disjoint s_1 (⋂ x, f ↑x ⋯)
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf ⟨b, a⟩ < sizeOf (a.cons' l)

Tactic:
simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]
  apply sizeof_pos

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

Goal state before:
pp: case inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
hba : b ≤ a
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.symm.lt_of_le hba) hb.le hf.symm

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

Goal state before:
pp: o : ONote
x✝ : NF 0
h₂ : o.NF
⊢ (0 - o).repr = repr 0 - o.repr

Tactic:
by cases o <;> exact (Ordinal.zero_sub _).symm

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card ≤ (V_ o).card

Tactic:
by
  simpa using card_mono o.toZFSet_subset_vonNeumann

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

Goal state before:
pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
revert p

Goal state after:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
⊢ (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m

Tactic:
revert p

Goal state after:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
⊢ (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m → o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
⊢ (o₁ ^ o₂).NF

Tactic:
have na := (nf_repr_split e₁).1

Goal state after:
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
⊢ (o₁ ^ o₂).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
o₁ : ONote
inst✝¹ : o₁.NF
b' : ONote
k : ℕ
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
inst✝ : NF 0
e₂ : split' 0 = (b', k)
⊢ (if True then zero.oadd ⟨1, ⋯⟩ zero else zero).NF

Tactic:
decide

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

Goal state before:
pp: 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
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : m = 0
⊢ (zero.oadd ⟨1, ⋯⟩ zero).NF

Tactic:
decide

Goal state after:
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} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
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 α'
⊢ ω0 ^ ↑k * a'.repr < ω ^ (a0.repr * succ ↑k)

Tactic:
opow_mul,

Goal state after:
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} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
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 α'
⊢ ω0 ^ ↑k * a'.repr < (ω ^ a0.repr) ^ succ ↑k
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist nil (Seq.cons x s) = 1

Tactic:
by
  rw [dist_comm]
  simp

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

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

Tactic:
opow_mul,

Goal state after:
case succ.refine_2.e_a.succ.ba
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) (k + 1) (n✝ + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(n✝ + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(n✝ + 1)) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ (ω ^ a0.repr) ^ succ ↑k ≤ ω0 ^ ↑k * α'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ω ^ b'.repr * ↑↑(m.succPNat ^ k) = (↑m + 1) ^ (ω * b'.repr) * (↑m + 1) ^ ↑k

Tactic:
opow_mul,

Goal state after:
case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ω ^ b'.repr * ↑↑(m.succPNat ^ k) = ((↑m + 1) ^ ω) ^ b'.repr * (↑m + 1) ^ ↑k
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
basis : Basis
h_allZero : AllZero []
⊢ Tendsto (toFun [] basis) atTop (𝓝 1)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: case h.nil
α : 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 α
hF :
  Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (h_opf.unfold s.head) =
    nil.destruct
⊢ (op nil).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head 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:
simp only [destruct_nil, Option.map_eq_none_iff] at hF

Goal state after:
case h.nil
α : 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 α
hF : h_opf.unfold s.head = none
⊢ (op nil).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head 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)))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.coef⁻¹ • (t.unit.toFun basis)⁻¹ =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹

Tactic:
filter_upwards [] with x

Goal state after:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ (t.coef⁻¹ • (t.unit.toFun basis)⁻¹) x = (t.coef • t.unit.toFun basis)⁻¹ x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_coef : coef = 0
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto 0 atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: case oadd.inl.none.inl.none.zero.right
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
⊢ (oadd 0 1 0).NF → NF 0

Tactic:
decide

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

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < 2 * 1

Tactic:
decide

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

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑1 = 1

Tactic:
decide

Goal state after:
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
⊢ b * l.prod = n

Tactic:
f₃,

Goal state after:
n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
⊢ b * m = n
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst

Tactic:
symm

Goal state after:
case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ ⟨fst, snd⟩.fst ≠ x
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[i]? = ys[j]?

Tactic:
symm

Goal state after:
case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = ys[i]?
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
x✝ : ℕ
n : ℕ := x✝
h : 0 < n
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
⊢ ‖c ^ (k + 1)‖ ≤ 1

Tactic:
grw [norm_pow, hc₁.le, one_pow]

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ IsOpen ↑I

Tactic:
rw [← Ideal.finprod_heightOneSpectrum_factorization hI,
    finprod_eq_finsetProd_of_mulSupport_subset _
      (s := (Ideal.hasFiniteMulSupport hI).toFinset) (by simp)]
  refine @AddSubgroup.isOpen_of_isClosed_of_finiteIndex _ _ _ _ (Submodule.toAddSubgroup _)
    ?_ (IsNoetherianRing.isClosed_ideal _)
  refine @AddSubgroup.finiteIndex_of_finite_quotient _ _ _ ?_
  refine Ideal.finite_quotient_prod _ _ (fun _ _ ↦ IsNoetherian.noetherian _) fun _ _ ↦ ?_
  exact Ideal.finite_quotient_pow (IsNoetherian.noetherian _) _

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
this : ∀ (m : ℕ) (j : cell C m), m < n
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨⟨m, ⋯⟩, j⟩)
    fun x ↦
    match x with
    | ⟨m, j⟩ => ⟨↑m, j⟩

Tactic:
simp [Function.RightInverse, Function.LeftInverse]

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

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ ∃ x ∈ Set.univ, ↑F ≤ 𝓝 x

Tactic:
refine ⟨X.str F, by tauto, ?_⟩

Goal state after:
X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ ↑F ≤ 𝓝 (X.str F)
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})
⊢ ∀ (Q₁ Q₂ : Finset ι),
    Q₁ ⊆ Q₂ → ⇑(π_app C fun x ↦ x ∈ Q₁) ⁻¹' {↑a (op Q₁)} ⊇ ⇑(π_app C fun x ↦ x ∈ Q₂) ⁻¹' {↑a (op Q₂)}

Tactic:
intro J K h x hx

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
hx : 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 : Set X
inst✝ : CWComplex C
e : cell C 1
⊢ ∃ x y, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y

Tactic:
by
  obtain ⟨f, h⟩ := cellFrontier_subset_finite_closedCell 1 e
  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
  obtain ⟨⟨u, hu, hun1⟩, v, hv, hv1⟩ := h
  use u, v
  simp [RelCWComplex.cellFrontier_one_eq, image_pair, RelCWComplex.closedCell_zero_eq_singleton,
    hun1, hv1, pair_comm]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
⊢ ∀ (c_1 : Products I),
    c c_1 ≠ 0 →
      e (π C fun x ↦ x ∈ s) a * c c_1 • Products.eval (π C fun x ↦ x ∈ s) c_1 ∈
        Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
intro m hm

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
⊢ e (π C fun x ↦ x ∈ s) a * c m • Products.eval (π C fun x ↦ x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
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 : ℕ∞
⊢ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply subset_antisymm
  · apply union_subset
    · exact subset_union_left
    · apply iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_
      apply subset_union_of_subset_right
      apply subset_iUnion₂_of_subset m hm
      apply subset_iUnion_of_subset j
      exact openCell_subset_closedCell m j
  · apply union_subset subset_union_left
    refine iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_
    rw [← cellFrontier_union_openCell_eq_closedCell]
    apply union_subset
    · induction m using Nat.case_strong_induction_on with
      | hz => simp [cellFrontier_zero_eq_empty]
      | hi m hm' =>
        obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j
        apply hI.trans
        apply union_subset subset_union_left
        apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun i _ ↦ ?_
        rw [← cellFrontier_union_openCell_eq_closedCell]
        apply union_subset
        · exact (hm' l (Nat.le_of_lt_succ hl) ((ENat.natCast_lt_natCast.2 hl).trans hm) i)
        · apply subset_union_of_subset_right
          exact subset_iUnion₂_of_subset l ((ENat.natCast_lt_natCast.2 hl).trans hm) <|
            subset_iUnion _ i
    · exact subset_union_of_subset_right (subset_iUnion₂_of_subset m hm (subset_iUnion _ j)) _

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

Goal state before:
pp: case neg.h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ ∀ (c_1 : Products I),
    c c_1 ≠ 0 →
      c c_1 • Products.eval (π C fun x ↦ x ∈ s) c_1 ∈
        Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
intro m hm

Goal state after:
case neg.h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
⊢ c m • Products.eval (π C fun x ↦ x ∈ s) m ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
⊢ Proj (fun x ↦ ord I x < o) x = x

Tactic:
by
  ext i
  simp only [Proj, ite_eq_left_iff, not_lt]
  intro hi
  rcases hi.lt_or_eq with hi | hi
  · specialize hsC x hx.1 i
    rw [← not_imp_not] at hsC
    simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC
    exact (hsC hi).symm
  · simp only [C0, Set.mem_inter_iff, Set.mem_ofPred_eq] at hx
    rw [eq_comm, ord_term ho] at hi
    rw [← hx.2, hi]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
⊢ ∃ y, (πs C o) y = f

Tactic:
let C₀C : C0 C ho → C := fun x ↦ ⟨x.val, x.prop.1⟩

Goal state after:
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
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
⊢ ∃ y, (πs C o) y = f
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Function.Injective (sum_to C ho)

Tactic:
by
  refine Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
    (fun ⟨a,ha⟩ ⟨b,hb⟩ ↦ (fun (hab : a = b) ↦ ?_))
  rw [← hab] at hb
  have ha' := Products.prop_of_isGood C _ ha (term I ho) hb.2
  simp only [ord_term_aux, lt_self_iff_false] at ha'

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC✝ : contained C (Order.succ o)
ho✝ : o < Ordinal.type fun x1 x2 ↦ x1 < x2
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (sum_to C ho) = GoodProducts C

Tactic:
sum_to_range C ho,

Goal state after:
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
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ GoodProducts (π C fun x ↦ ord I x < o) ∪ MaxProducts C ho = GoodProducts C