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

Goal state before:
pp: p n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑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)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n

Tactic:
have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by norm_cast
  rw [wittPolyProd, wittPolynomial, map_sum, map_sum]
  conv_lhs =>
    arg 1
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
  conv_lhs =>
    arg 2
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
  conv_rhs =>
    enter [1, 1, 2, 2]
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
  conv_rhs =>
    enter [1, 2, 2]
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
  simp only [add_mul, mul_add]
  rw [add_comm _ (remainder p n)]
  simp only [add_assoc]
  apply congrArg (Add.add _)
  ring

Goal state after:
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case refine_2
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ F₀.range = K(p, k) ∙ x

Tactic:
rw [LinearMap.span_singleton_eq_range]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
⊢ IsClub (⋂₀ s)

Tactic:
refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, fun a ↦ ?_⟩

Goal state after:
case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
⊢ ∃ y ∈ ⋂₀ s, a ≤ y
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),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
obtain ⟨f, hf⟩ := nth_mul_coeff' p k n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (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)
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
hs : ¬IsCofinal sᶜ
⊢ IsStationary s

Tactic:
by
  intro t ht
  obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs
  obtain ⟨b, hb, hb'⟩ := ht.isCofinal a
  refine ⟨b, ?_, hb⟩
  contrapose! ha
  exact ⟨b, ha, hb'⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
⊢ AccPt a (𝓟 s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

Tactic:
accPt_iff_frequently

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case neg
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∉ f.support
⊢ f e' < b

Tactic:
rw [notMem_support_iff.1 he']
        exact hb.pos

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

Goal state before:
pp: case inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
rw [ite_eq_iff] at nh; rcases nh.right with nh | nh <;> cases nh <;> contradiction

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

Goal state before:
pp: case oadd.lt.h₁
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝² : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝¹ : e.NF
this✝ : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ e'.repr
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr

Tactic:
cases he' : e' <;>
          simp only [he', zero_def, opow_zero, repr, repr_zero, gt_iff_lt] at this ⊢

Goal state after:
case oadd.lt.h₁.zero
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝² : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝¹ : e.NF
this✝ : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
he' : e' = zero
this : ω ^ e.repr * ↑↑n + a.repr < 1
⊢ ω ^ e.repr * ↑↑n < 1

case oadd.lt.h₁.oadd
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝² : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝¹ : e.NF
this✝ : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
he' : e' = a✝².oadd a✝¹ a✝
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ (ω ^ a✝².repr * ↑↑a✝¹ + a✝.repr)
⊢ ω ^ e.repr * ↑↑n < ω ^ (ω ^ a✝².repr * ↑↑a✝¹ + a✝.repr)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
i : α
⊢ f i ⊆ ⋃ (i : α), f i

Tactic:
by
  intro x hx
  simpa using ⟨i, hx⟩

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

Goal state before:
pp: case h
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x

Tactic:
| _ x ih
   => 

Goal state after:
case h
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
h : e₁.cmp e₂ = Ordering.eq
this : e₁ = e₂
⊢ (match Ordering.eq 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₁).NFBelow
    b

Tactic:
subst e₂

Goal state after:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
⊢ (match Ordering.eq 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₁).NFBelow
    b
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ x.powerset
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x.powerset

Tactic:
rw [mem_powerset] at hy ⊢
  exact h.subset_of_mem (hy hz)

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

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

Tactic:
| _ x ih
   => 

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

Goal state before:
pp: case eq
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
h : e₁.cmp e₂ = Ordering.eq
ee : e₁ = e₂
⊢ (match Ordering.eq 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 =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
subst e₂

Goal state after:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
⊢ (match Ordering.eq 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 =
    (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hz : z ⊆ V_ a
⊢ z.rank < o

Tactic:
exact (subset_vonNeumann.1 hz).trans_lt ha

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

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).NF

Tactic:
have h' : o₂ ≠ zero := fun he => h (he ▸ zero_def ▸ rfl)
        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one,
          h', ite_false]
        exact NF.zero

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

Goal state before:
pp: 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
h : a'.repr + ↑0 < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (k + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) k 0).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑0) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ R = 0

Tactic:
cases k <;> simp [R, opowAux]

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

Goal state before:
pp: hd : ℝ → ℝ
tl : Basis
h : WellFormedBasis (hd :: tl)
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
rw [WellFormedBasis, List.pairwise_cons] at h

Goal state after:
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)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ m.inv.toFun basis =ᶠ[atTop] (m.toFun basis)⁻¹

Tactic:
by
  eta_expand
  simp only [toFun, inv, Pi.inv_apply]
  induction m generalizing basis with
  | nil => simp
  | cons exp exps ih =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
· have h_eq : UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =
                    UnitMonomial.toFun exps_tl basis_tl := by
          ext x; simp [UnitMonomial.toFun, h.left]
        rw [h_eq]
        exact toFun_tendsto_top_of_firstNonzeroIsPos h_basis.tail (by simpa using h_length) h.right

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
left right : Basis
⊢ let t := { coef := coef, unit := List.replicate (List.length left) 0 ++ exps };
  t.toFun (left ++ right) = { coef := coef, unit := exps }.toFun right

Tactic:
exact congrArg (coef • ·) UnitMonomial.zeros_append_toFun

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (Multiseries.cons exp coef tl).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
exact h.elim_cons

Goal state after:
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : 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

Tactic:
apply eq_zero_of_pow_eq_zero (n := n)

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') ^ n = 0
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
Int.ModEq,

Goal state after:
case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a % ↑n = ↑(a % ↑n).toNat % ↑n
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a % ↑n = a % ↑n % ↑n

Tactic:
emod_emod

Goal state after:
case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a % ↑n = a % ↑n
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
d : ℕ
hd : IsSquare d
n : ℕ
ha : IsNNRat a (n * n) d
⊢ IsSquare a

Tactic:
rcases hd with ⟨d, rfl⟩

Goal state after:
a : ℚ
n d : ℕ
ha : IsNNRat a (n * n) (d * d)
⊢ IsSquare a
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ -(↑n / ↑d) < 0

Tactic:
by rw [Left.neg_neg_iff]; apply div_pos <;> simpa [Nat.pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: case mk.mk
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(⟨val✝¹, property✝¹⟩ - ⟨val✝, property✝⟩) = ↑⟨val✝¹, property✝¹⟩ - 1 - ↑⟨val✝, property✝⟩ + 1

Tactic:
simp only [PNat.mk_coe, _root_.PNat.sub_coe, ← _root_.PNat.coe_lt_coe]

Goal state after:
case mk.mk
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
⊢ (if val✝ < val✝¹ then val✝¹ - val✝ else 1) = val✝¹ - 1 - val✝ + 1
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ a✝ ^ ↑b = ↑((a.pow b).mod n)

Tactic:
rw [h, Nat.cast_id, Nat.pow_eq, ← Nat.cast_pow, CharP.natCast_eq_natCast_mod α n]

Goal state after:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b % n) = ↑((a ^ b).mod n)
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
s : Set G
⊢ (Subgroup.closure s).topologicalClosure = (Submonoid.closure s).topologicalClosure

Tactic:
refine le_antisymm ?_ (closure_mono <| Subgroup.le_closure_toSubmonoid _)

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).topologicalClosure ≤ (Submonoid.closure s).topologicalClosure
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ Proj J ∘ Proj K '' C

Tactic:
refine ⟨y, hy, ?_⟩

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ (Proj J ∘ Proj K) y = Proj J y
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)
y : I → Bool
hy : y ∈ C
⊢ (fun i ↦ ↑⟨Proj J y, ⋯⟩ ↑i) ∈ IndexFunctor.obj C J

Tactic:
refine ⟨y, hy, ?_⟩

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)
y : I → Bool
hy : y ∈ C
⊢ (precomp Subtype.val) y = fun i ↦ ↑⟨Proj J y, ⋯⟩ ↑i
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
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ord I i < o → ord I i = o → true = ↑x i

Tactic:
intro h₁ h₂

Goal state after:
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
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
i : I
h₁ : ord I i < o
h₂ : ord I i = o
⊢ true = ↑x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
⊢ Submodule.span ℤ (eval {fun x ↦ false} '' {nil}) = ⊤

Tactic:
by
  rw [Set.image_singleton, eq_top_iff]
  intro f _
  rw [Submodule.mem_span_singleton]
  refine ⟨f default, ?_⟩
  simp only [eval, List.map, List.prod_nil, zsmul_eq_mul, mul_one, Products.nil]
  ext x
  obtain rfl : x = default := by simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]
  rfl

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

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x ↦ ord I x < o))
hab : (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a = (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) b
⊢ a = b

pp: case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
hb : b ∈ range (π C fun x ↦ ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩

Tactic:
· ext1
    simp only [Subtype.mk.injEq] at hab
    exact injective_πs C o hab

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
hb : b ∈ range (π C fun x ↦ ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ (e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * (eval C l.Tail) ⟨SwapTrue o ↑x, ⋯⟩ -
      (e C (term I ho)) (CC'₀ C ho x) * (eval C l.Tail) (CC'₀ C ho x) =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x

Tactic:
CC'₀,

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ (e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * (eval C l.Tail) ⟨SwapTrue o ↑x, ⋯⟩ -
      (e C (term I ho)) ⟨↑x, ⋯⟩ * (eval C l.Tail) ⟨↑x, ⋯⟩ =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x
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 : ℕ∞
x : X
⊢ (x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n + 1), ∃ j, x ∈ openCell m j) ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
suffices ∀ (m : ℕ), m < n + 1 ↔ m ≤ n by simp_rw [this]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
x : X
⊢ ∀ (m : ℕ), ↑m < n + 1 ↔ ↑m ≤ n
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ¬∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ 0 = 1

Tactic:
push Not at h₁; obtain ⟨i, hi⟩ := h₁; exfalso; rw [← hi' i hi.1] at hi; exact hi.2 (h₃ i hi.1)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t

Tactic:
hT.open_eq_sUnion' hU,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K (⋃₀ {s | s ∈ T ∧ s ⊆ U})
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t