mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ ∀ (i : { b // b ∈ x }), succ (lift.{u + 1, u} (↑i).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
intro h

Goal state after:
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : { b // b ∈ x }
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
rintro ⟨w, hwx, z, rfl, hwz⟩

Goal state after:
case mpr
x w : Class.{u}
hwx : w ∈ x
z : ZFSet.{u}
hwz : w z
⊢ ↑z ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case mp
x : ZFSet.{u}
⊢ x.IsTransitive → ⋃₀ x ⊆ x

Tactic:
intro h

Goal state after:
case mp
x : ZFSet.{u}
h : x.IsTransitive
⊢ ⋃₀ x ⊆ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case mpr
x : ZFSet.{u}
⊢ ⋃₀ x ⊆ x → x.IsTransitive

Tactic:
intro h

Goal state after:
case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
⊢ x.IsTransitive
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ ∀ c < lift.{u + 1, u} x.rank, c < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

Tactic:
intro h

Goal state after:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ ∀ (i : ↥x), succ (lift.{u + 1, u} (↑i).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
intro h

Goal state after:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : ↥x
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
constructor
  · revert hx hy
    refine Sym2.GameAdd.recursion mem_wf ?_ x y
    intro x y IH hx hy hxy
    by_cases hyx : y ⊆ x
    · exact Or.inl (subset_antisymm hxy hyx)
    · obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y \ x) (Set.sdiff_nonempty.2 hyx)
      have hmy : m ∈ y := by simp only [Set.mem_sdiff, SetLike.mem_coe] at hm; exact hm.1
      have hmx : m ⊆ x := by
        intro z hzm
        by_contra hzx
        exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm
      obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx
      · exact Or.inr hmy
      · cases Set.notMem_of_mem_sdiff hm H
  · rintro (rfl | h)
    · rfl
    · exact hy.subset_of_mem h

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

Goal state before:
pp: o : Ordinal.{u_1}
z : ZFSet.{u_1}
⊢ z ∈ V_ (o + 1) ↔ z ∈ (V_ o).powerset

Tactic:
mem_vonNeumann,

Goal state after:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
⊢ z.rank < o + 1 ↔ z ∈ (V_ o).powerset
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ IsNat ((algebraMap R A) (r + 0)) 1

Tactic:
simp only [h.out, Nat.cast_one, add_zero, map_one]

Goal state after:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ IsNat 1 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g basis_hd : ℝ → ℝ
exp✝ : ℝ
hf : Majorized f basis_hd exp✝
hg : g =O[atTop] fun x ↦ 1
exp : ℝ
h_exp : exp > exp✝
⊢ (f * g) =o[atTop] (basis_hd ^ exp)

Tactic:
convert! IsLittleO.mul_isBigO (hf _ h_exp) hg using 1

Goal state after:
case e'_8
f g basis_hd : ℝ → ℝ
exp✝ : ℝ
hf : Majorized f basis_hd exp✝
hg : g =O[atTop] fun x ↦ 1
exp : ℝ
h_exp : exp > exp✝
⊢ basis_hd ^ exp = fun x ↦ (basis_hd ^ exp) x * 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case neg
α : Type u_1
s t : Stream' α
h : ¬s = t
⊢ dist s t ≤ 1

Tactic:
rw [PiNat.dist_eq_of_ne h]

Goal state after:
case neg
α : Type u_1
s t : Stream' α
h : ¬s = t
⊢ (1 / 2) ^ PiNat.firstDiff s t ≤ 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
x : α
s t : Stream'.Seq α
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
by_cases! h : s = t
  · simp [h]
  have h' : cons x s ≠ cons x t := by
    simpa
  rw [Subtype.dist_eq, Subtype.dist_eq, PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h),
    PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h')]
  simp only [show (1 / 2 : ℝ) = 2⁻¹ by simp, ← pow_succ']
  congr
  simp only [val_cons, PiNat.firstDiff, ne_eq, Classical.dite_not, Subtype.coe_ne_coe.mpr h,
    not_false_eq_true, ↓reduceDIte, val_eq_get]
  split_ifs with h_if
  · contrapose! h'
    apply_fun Subtype.val using Subtype.val_injective
    simpa
  · convert! Nat.find_comp_succ _ _ _
    simp [Stream'.cons]

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

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

Tactic:
by
  apply dist_eq_one_of_head
  simp

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

Goal state before:
pp: case cons.inr
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
· simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
      exact .trans (by grind) h_comp

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

Goal state before:
pp: hd : ℝ → ℝ
tl : Basis
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    ∀ f ∈ hd :: tl, Tendsto f atTop atTop
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
exact h.left.left _ hf

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹ * dist x y
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
grw [dist_le_one x y, mul_one] at h

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
⊢ cons exp coef tl ≠ nil

Tactic:
intro h

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : cons exp coef tl = nil
⊢ False
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun
⊢ ms₁ = ms₂

Tactic:
rw [eq_mk ms₁, eq_mk ms₂]
    simp [h]

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

Goal state before:
pp: n k d : ℕ
h_left : k ^ d < n
h_right : n < (k + 1) ^ d
m : ℕ
⊢ n ≠ m ^ d

Tactic:
intro h

Goal state after:
n k d : ℕ
h_left : k ^ d < n
h_right : n < (k + 1) ^ d
m : ℕ
h : n = m ^ d
⊢ False
Module: Mathlib.Tactic.NormNum.LegendreSymbol

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

Tactic:
by decide

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Ico ⊥ (n + 1) = s

Tactic:
Ico_add_one_right_eq_Icc,

Goal state after:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Icc ⊥ n = s
Module: Mathlib.Testing.Plausible.Functions

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

Tactic:
intro h

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A).getD 0 = 0
⊢ ∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case some.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
ys : List α
h₀ : (x' :: xs).Nodup
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip ys)) = some val
h₂ : ys.Nodup
h₁ : (x' :: xs).length = ys.length
⊢ val ∈ ys ↔ x ∈ x' :: xs

Tactic:
rcases ys with - | ⟨y, ys⟩

Goal state after:
case some.cons.nil
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip [])) = some val
h₂ : [].Nodup
h₁ : (x' :: xs).length = [].length
⊢ val ∈ [] ↔ x ∈ x' :: xs

case some.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip (y :: ys))) = some val
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
⊢ x ∉ xs → applyId (xs.zip ys) x = x

Tactic:
intro h

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ applyId (xs.zip ys) x = 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[j]? = some (List.applyId (xs.zip ys) y)

Tactic:
rw [← List.applyId_zip_eq]

Goal state after:
case pos.e_a.h₀
α : 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
⊢ xs.Nodup

case pos.e_a.h₁
α : 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
⊢ xs.length = ys.length

case pos.e_a.h₂
α : 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
⊢ xs[j]? = some y
Module: Mathlib.Testing.Plausible.Functions

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

Tactic:
by decide

Goal state after:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt x atTop fun x_1 ↦ x ^ x_1

Tactic:
simpa using mapClusterPt_self_zpow_atTop_pow x 1

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
⊢ f ⋆[L] g = g ⋆[L] f

Tactic:
by
  unfold convolution; ext x
  rw [← (mulFiber_swapEquiv x).tsum_eq]
  congr 1; funext ⟨⟨a, b⟩, _⟩; exact hL (f b) (g a)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ (fun y ↦ 1 + y) x ∈ s

Tactic:
refine hn' this.unit (by simpa using hx) ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ -1 + ↑this.unit⁻¹ ∈ I ^ n
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 • p.2

Tactic:
let t₁ : TopologicalSpace E := .induced (B · ·) Pi.topologicalSpace
    have : B.IsWeak := ⟨rfl⟩
    rw [hB.eq_induced, continuous_induced_rng]
    simp only [Function.comp_def, map_smul, smul_apply]
    fun_prop

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✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
⊢ Finite R

Tactic:
have H : (∏ p : PrimeSpectrum R, p.asIdeal) ^ n = ⊥ := by
    rw [← le_bot_iff, ← Ideal.zero_eq_bot, ← hn]
    gcongr
    rw [Ideal.jacobson_bot, Ring.jacobson_eq_sInf_isMaximal, le_sInf_iff]
    exact fun I hI ↦ Ideal.prod_le_inf.trans
      (Finset.inf_le (b := PrimeSpectrum.mk I hI.isPrime) (by simp))

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
H : (∏ p, p.asIdeal) ^ n = ⊥
⊢ Finite R
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
⊢ (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D) →
    IsClosed[inst✝] A

Tactic:
intro h

Goal state after:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
⊢ IsClosed[inst✝] A
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell i i_1
⊢ x ∉ D → ∃ i < n, ∃ i_1 ∈ E.I i, i_1 ∈ J i ∧ x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1

Tactic:
intro h

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell i i_1
h : x ∉ D
⊢ ∃ i < n, ∃ i_1 ∈ E.I i, i_1 ∈ J i ∧ x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ ↑F ≤ 𝓝 (X.str F)

Tactic:
le_nhds_iff

Goal state after:
X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False

Tactic:
le_nhds_iff

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ∀ (s : Set X.A), x ∈ s → IsOpen s → s ∈ ↑F
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
⊢ ↑F ≤ 𝓝 (X.str F)

Tactic:
le_nhds_iff

Goal state after:
X : Compactum
F : Ultrafilter X.A
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F
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
⊢ ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x

Tactic:
le_nhds_iff

Goal state after:
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
⊢ ∀ (s : Set X), x ∈ s → IsOpen[inst✝²] s → s ∈ ↑(Ultrafilter.map Ultrafilter.lim FF)
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)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x✝ : (Finset I)ᵒᵖ
s : Finset I
a✝ : ↑(((Functor.const (Finset I)ᵒᵖ).obj (indexCone hC).pt).obj (op s)).toTop
⊢ (ConcreteCategory.hom ((indexCone hC).π.app (op s))) a✝ =
    (ConcreteCategory.hom
        ((Iso.refl (indexCone hC).pt).hom ≫
          ((Cone.postcompose (spanFunctorIsoIndexFunctor hC).hom).obj (spanCone hC)).π.app (op s)))
      a✝

Tactic:
have : iso_map C (· ∈ s) ∘ ProjRestrict C (· ∈ s) = IndexFunctor.π_app C (· ∈ s) := by
        ext _ i; exact dif_pos i.prop

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)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x✝ : (Finset I)ᵒᵖ
s : Finset I
a✝ : ↑(((Functor.const (Finset I)ᵒᵖ).obj (indexCone hC).pt).obj (op s)).toTop
this : (⇑(iso_map C fun x ↦ x ∈ s) ∘ ProjRestrict C fun x ↦ x ∈ s) = ⇑(IndexFunctor.π_app C fun x ↦ x ∈ s)
⊢ (ConcreteCategory.hom ((indexCone hC).π.app (op s))) a✝ =
    (ConcreteCategory.hom
        ((Iso.refl (indexCone hC).pt).hom ≫
          ((Cone.postcompose (spanFunctorIsoIndexFunctor hC).hom).obj (spanCone hC)).π.app (op s)))
      a✝
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 := ⋯
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:
le_nhds_iff

Goal state after:
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)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hz
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
j : cell C 0
⊢ IsClosed[t] (A ∩ closedCell 0 j)

Tactic:
rw [closedCell_zero_eq_singleton]

Goal state after:
case hz
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
j : cell C 0
⊢ IsClosed[t] (A ∩ {↑(map 0 j) ![]})