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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Tactic:
by
  simp only [← peval_polyOfInterest']
  obtain ⟨f₀, hf₀⟩ := exists_restrict_to_vars (s := SetLike.coe (univ ×ˢ range (n + 1))) k
    (polyOfInterest_vars p n)
  let f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k := by
    intro x y
    apply f₀
    rintro ⟨a, ha⟩
    apply Function.uncurry ![x, y]
    let S : Set (Fin 2 × ℕ) := { a | a.2 = n ∨ a.2 < n }
    have ha' : a ∈ S := by grind
    refine ⟨a.fst, ⟨a.snd, ?_⟩⟩
    obtain ⟨ha, ha⟩ := ha' <;> lia
  use f
  intro x y
  dsimp [f, peval]
  rw [← hf₀]
  congr
  ext a
  obtain ⟨a, ha⟩ := a
  obtain ⟨i, m⟩ := a
  fin_cases i <;> rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
this✝ : Nonempty α
hα : IsCofinal (range (rangeSplitting f))
this : LinearOrder ↑(range f) := ⋯.linearOrder
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #β

Tactic:
← lift_cof_congr_of_strictMono (rangeSplitting_strictMono hf) hα,

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
this✝ : Nonempty α
hα : IsCofinal (range (rangeSplitting f))
this : LinearOrder ↑(range f) := ⋯.linearOrder
⊢ lift.{u, v} (cof ↑(range f)) ≤ lift.{u, v} #β
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
⊢ ∀ ⦃s : Set (Set (List A))⦄,
    s ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T} → sSup s ∈ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}

Tactic:
rintro S hS x a ⟨t, ht, hx⟩

Goal state after:
A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
t : Set (List A)
ht : t ∈ S
hx : x ++ [a] ∈ t
⊢ x ∈ sSup S
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inr
A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : w✝ ∈ subAt T x
h' : x.length ≤ (x ++ w✝).length
⊢ x ++ w✝ ∈ ↑T

Tactic:
exact h

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ lfpApprox f x 0 = x

Tactic:
by
  rw [lfpApprox]
  simp

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := ⋯ ▸ b;
    ofList l'.toList = l'
IH :
  ∀ (h : true = true),
    let l' := ⋯ ▸ a;
    ofList l'.toList = l'
h : true = true
⊢ let l' := ⋯ ▸ b.cons' a;
  ofList l'.toList = l'

Tactic:
simpa [cons] using IH rfl

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (map Prod.toSigma (CNF b o)).NodupKeys

Tactic:
by
  rw [NodupKeys, List.keys, map_map, Prod.fst_comp_toSigma]
  exact (CNF.sortedGT ..).nodup

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

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

Tactic:
ext; simpa using @hyx _

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

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

Tactic:
by ext; simpa using @hyx _

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

Goal state before:
pp: x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
intro _ ⟨_, _, _⟩

Goal state after:
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : ZFSet.{u_1}
⊢ ∀ ⦃y : ZFSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
intro _ ⟨_, _, _⟩

Goal state after:
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case refine_1
x : ZFSet.{u}
hx : ↑x = IsOrdinal
y : ZFSet.{u}
hy : y ∈ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x

Tactic:
← Class.coe_apply,

Goal state after:
case refine_1
x : ZFSet.{u}
hx : ↑x = IsOrdinal
y : ZFSet.{u}
hy : ↑x y
z : ZFSet.{u}
hz : ↑y z
⊢ ↑x z
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case refine_2
x : ZFSet.{u}
hx : ↑x = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : y✝ ∈ z✝
hzw : z✝ ∈ w✝
hwx : w✝ ∈ x
⊢ y✝ ∈ w✝

Tactic:
← Class.coe_apply,

Goal state after:
case refine_2
x : ZFSet.{u}
hx : ↑x = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : ↑z✝ y✝
hzw : ↑w✝ z✝
hwx : ↑x w✝
⊢ ↑w✝ y✝
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
⊢ Tendsto f (𝓝[<] c) l

Tactic:
convert_to Tendsto (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l at h

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
⊢ (fun x ↦ f (c - x⁻¹)) = f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv

α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l
⊢ Tendsto f (𝓝[<] c) l
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

Goal state after:
case cons.inr
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
h :
  ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
⊢ LipschitzWith 2⁻¹ F

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
this : ∃ C, ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ BddAbove (Set.range fun b ↦ dist (f b) (g b))

Tactic:
obtain ⟨C, hC⟩ := this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ BddAbove (Set.range fun b ↦ dist (f b) (g b))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case cons
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : WellFormedBasis tl → ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h : WellFormedBasis (hd :: tl)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x

Tactic:
simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h

Goal state after:
case cons
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : WellFormedBasis tl → ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
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) ∧
    Tendsto hd atTop atTop ∧ ∀ a ∈ tl, Tendsto a atTop atTop
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
n : ℕ
r : ℝ
⊢ (Multiseries.monomialRpow basis_hd basis_tl n r).Sorted

Tactic:
cases n with
  | zero =>
    simp only [Multiseries.monomialRpow]
    exact Sorted.cons_nil const_sorted
  | succ m =>
    simp only [Multiseries.monomialRpow]
    exact Sorted.cons_nil monomialRpow_sorted

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

Goal state before:
pp: case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ ↑(k + 1)

Tactic:
exact (repr_opow_aux₂ _ ad a00 al _ _).2

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
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ (op ms).destruct =
    Option.map
      (fun x ↦
        match x with
        | (exp, coef, op') => (exp, coef, ↑op' ms.tail))
      (h.unfold ms.head)

Tactic:
unfold Multiseries.destruct

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ Option.map
      (fun x ↦
        match x with
        | ((exp, coef), tl) => (exp, coef, tl))
      (Seq.destruct (op ms)) =
    Option.map
      (fun x ↦
        match x with
        | (exp, coef, op') => (exp, coef, ↑op' ms.tail))
      (h.unfold ms.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.right.cons.right
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).Sorted

Tactic:
· exact Sorted.seq _ (fun x hx ↦ h_coef _ (by simp_all)) h_Pairwise

Goal state after:
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]

Tactic:
Nat.ModEq,

Goal state after:
case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n = a % n % n
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y ∣ a

Tactic:
· exact eq_of_mul_eq_mul_of_coprime_aux (x := b) hxy.symm (by rw [mul_comm, ← h, mul_comm])

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

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

Tactic:
by
  simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
  rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]
  rw [← Nat.mod_mod_of_dvd, hb]; simp

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

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

Tactic:
by
  simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
  rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]
  rw [← Nat.mod_mod_of_dvd, hb]; simp

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

Goal state before:
pp: G : GrpCat
g : ↑G
⊢ (ConcreteCategory.hom (eta G)) g = 1 ↔ ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H

Tactic:
rw [Subtype.ext_iff, funext_iff]

Goal state after:
G : GrpCat
g : ↑G
⊢ (∀ (x : FiniteIndexNormalSubgroup ↑G), ↑((ConcreteCategory.hom (eta G)) g) x = ↑1 x) ↔
    ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
f : InjectiveFunction α
⊢ Injective f.apply

Tactic:
by
  obtain ⟨xs, hperm, hnodup⟩ := f
  generalize h₀ : List.map Sigma.fst xs = xs₀
  generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁
  dsimp [id] at h₁
  have hxs : xs = TotalFunction.List.toFinmap' (xs₀.zip xs₁) := by
    rw [← h₀, ← h₁, List.toFinmap']; clear h₀ h₁ xs₀ xs₁ hperm hnodup
    induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih
  revert hperm hnodup
  rw [hxs]; intro hperm hnodup
  apply InjectiveFunction.applyId_injective
  · rwa [← h₀, hxs, hperm.nodup_iff]
  · rwa [← hxs, h₀, h₁] at hperm

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:
by grw [norm_pow, hc₁.le, one_pow]

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

Goal state before:
pp: case hab
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
⊢ ∏ p, p.asIdeal ≤ Ring.jacobson R

Tactic:
Ring.jacobson_eq_sInf_isMaximal,

Goal state after:
case hab
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
⊢ ∏ p, p.asIdeal ≤ sInf {I | I.IsMaximal}
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 : _root_.Finite ((n : ℕ) × cell C n)
h✝¹ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
a✝ : A.max' ⋯ + 1 ≤ m
j : cell C m
h✝ : True
⊢ ∃ a, a.fst = m

Tactic:
use ⟨m, j⟩

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set (WithGeneratedByTopology X Y)
⊢ IsClosed U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' U)

Tactic:
by
  simp [isClosed_iSup_iff, isClosed_coinduced, equiv, Equiv.refl]

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

Goal state before:
pp: case refine_1
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a b : (fun X ↦ ↑X.toTop) (indexCone hC).pt
J : Finset ι
h :
  ↑((ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a) (op J) =
    ↑((ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) b) (op J)
⊢ (π_app C fun x ↦ x ∈ J) a = (π_app C fun x ↦ x ∈ J) b

Tactic:
exact h

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
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
x✝ : I
⊢ ↑y x✝ = ↑x x✝

Tactic:
apply h

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

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑g ≤ 𝓝 x

Tactic:
apply h

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

Goal state before:
pp: D : CompHaus
x✝ : Set ↑D.1
h : ∀ (F : Ultrafilter ↑D.1), F.lim ∈ x✝ → x✝ ∈ ↑F
⊢ IsOpen (id ⁻¹' x✝)

Tactic:
exact h

Goal state after:
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]
    exact isClosed_inter_singleton

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ False

Tactic:
apply h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) []

Tactic:
simp only [List.isChain_nil]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
⊢ False

Tactic:
apply h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
⊢ eval C l ∈ Submodule.span ℤ (eval C '' {m | m < l})
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
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
⊢ False

Tactic:
apply h

Goal state after:
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
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
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
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
hh' : ∀ a ∈ ↑l, ord I a < o
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Tactic:
Products.eval_πs_image C hh',

Goal state after:
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
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
hh' : ∀ a ∈ ↑l, ord I a < o
⊢ Products.eval C l ∈ Submodule.span ℤ (⇑(πs C o) '' Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ Disjoint (interior D) (closedCell n j)

Tactic:
disjoint_iff_inter_eq_empty

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ interior D ∩ closedCell n j = ∅
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
⊢ ∀ (i : ℕ), C i ∈ insert ∅ S

Tactic:
by simp [hi]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
contra : v = 0
⊢ False

Tactic:
by simp [contra] at hv

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ (∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅) ↔
    ∀ (C : ℕ → Set α),
      Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty

Tactic:
refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h3 : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
h4 : ∀ (i : ℕ), C i ∈ S
⊢ (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty

case refine_2
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
h3 : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
s : ∀ (i : ℕ), C i ∈ S
⊢ ⋂ i, C i = ∅ → ∃ n, C n = ∅
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
exact ⟨fun h ↦ False.elim <| (h.trans_le hM).not_ge (by positivity),
      fun h ↦ False.elim <| (h (Classical.arbitrary α) |>.trans_le hM).not_ge (by positivity)⟩

Goal state after: