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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ n * wittMul p n + wittPolyProdRemainder p n = ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i)

Tactic:
rw [sum_range_succ, add_comm, Nat.sub_self, pow_zero, pow_one]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProdRemainder p n + ↑p ^ n * wittMul p n =
    ∑ x ∈ range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Tactic:
have hq0 : q ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.1 hq

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
this : NeZero (p - 1)
⊢ HasEnoughRootsOfUnity (ZMod p) (p - 1)

Tactic:
refine HasEnoughRootsOfUnity.of_card_le ?_

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : NeZero (p - 1)
⊢ p - 1 ≤ Nat.card ↥(rootsOfUnity (p - 1) (ZMod p))
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ CNF b o = [(0, o)]

Tactic:
rw [CNF.ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, zero_right]

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

Goal state before:
pp: b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ e ∉ (coeff b o).support

Tactic:
support_coeff,

Goal state after:
b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ e ∉ (map Prod.fst (CNF b o)).toFinset
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = (single e x) e + (coeff b y) e

Tactic:
rw [single_eq_same, coeff_eq_zero_of_lt hy, add_zero]

Goal state after:
case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = x
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
h : IsMin a
⊢ 𝓝 a = pure a

Tactic:
rw [nhds_eq_pure, isSuccLimit_iff]

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
h : IsMin a
⊢ ¬(¬IsMin a ∧ IsSuccPrelimit a)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ eval b (single e₁ x + f₁ + f₂) = eval b (single e₁ x + f₁) + eval b f₂

Tactic:
add_assoc,

Goal state after:
case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ eval b (single e₁ x + (f₁ + f₂)) = eval b (single e₁ x + f₁) + eval b f₂
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p * (coeff b o) p + r) 0 ((coeff b o).support.sort fun x1 x2 ↦ x1 ≥ x2) =
    foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)

Tactic:
support_coeff,

Goal state after:
b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p * (coeff b o) p + r) 0 ((map Prod.fst (CNF b o)).toFinset.sort fun x1 x2 ↦ x1 ≥ x2) =
    foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case 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
nf : (a.add o).NF
h : a.add o = zero
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

Tactic:
simp only [add, addAux, h'.symm, h, add_assoc, repr] at nf h₁ ⊢

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

Goal state before:
pp: case 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
nf : (a.add o).NF
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

Tactic:
simp only [add, addAux, h'.symm, h, add_assoc, repr] at nf h₁ ⊢

Goal state after:
case 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
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₂ ≤ o₁
⊢ veblenWith f o₂ a < veblenWith f o₁ (veblenWith f o₂ a) ↔ a < veblenWith f o₁ a

Tactic:
(right_le_veblenWith hf ..).lt_iff_ne',

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₂ ≤ o₁
⊢ veblenWith f o₁ (veblenWith f o₂ a) ≠ veblenWith f o₂ a ↔ veblenWith f o₁ a ≠ a
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a.h₁
x y : ZFSet.{u_1}
⊢ x ⊆ x ∪ y

Tactic:
intro _ h

Goal state after:
case a.h₁
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ x
⊢ x✝ ∈ x ∪ y
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case h₂
x y : ZFSet.{u_1}
⊢ y ⊆ x ∪ y

Tactic:
intro _ h

Goal state after:
case h₂
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ y
⊢ x✝ ∈ x ∪ y
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (Γ_ o).invVeblen₁ = Γ_ o

Tactic:
← veblen_gamma_zero,

Goal state after:
o : Ordinal.{u_1}
⊢ (veblen (Γ_ o) 0).invVeblen₁ = veblen (Γ_ o) 0
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (Γ_ o).invVeblen₂ = 0

Tactic:
← veblen_gamma_zero,

Goal state after:
o : Ordinal.{u_1}
⊢ (veblen (Γ_ o) 0).invVeblen₂ = 0
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case neg
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
⊢ x = y ∨ x ∈ y

Tactic:
obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx

Goal state after:
case neg.inl
x y✝ y : ZFSet.{u}
hy : y.IsOrdinal
m : ZFSet.{u}
hmy : m ∈ y
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(m, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : m.IsOrdinal
hxy : m ⊆ y
hyx : ¬y ⊆ m
hm : m ∈ ↑y \ ↑m
hm' : ∀ x ∈ ↑y \ ↑m, x ∉ m
hmx : m ⊆ m
⊢ m = y ∨ m ∈ y

case neg.inr
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y
Module: Mathlib.Tactic.AddGroup

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

Tactic:
add_assoc,

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

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

Tactic:
add_assoc,

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

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

Tactic:
_neg_zsmul_trick

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

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

Tactic:
add_assoc,

Goal state after:
G : Type u_1
inst✝ : AddGroup G
a b : G
⊢ a + (-b + -b) = a + -2 • b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.succ
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
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ ω ^ e₁.repr * ↑(succ n✝) + a₁.repr =
    ω ^ e₁.repr * ↑↑n₂ + ω ^ e₁.repr * ↑(n✝ + 1) + a₁.repr - (ω ^ e₁.repr * ↑↑n₂ + a₂.repr)

Tactic:
add_assoc,

Goal state after:
case eq.succ
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
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ ω ^ e₁.repr * ↑(succ n✝) + a₁.repr =
    ω ^ e₁.repr * ↑↑n₂ + (ω ^ e₁.repr * ↑(n✝ + 1) + a₁.repr) - (ω ^ e₁.repr * ↑↑n₂ + a₂.repr)
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
h : a ≤ b
x : ZFSet.{u_1}
hx : x ∈ a.toZFSet
⊢ x ∈ b.toZFSet

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hx

Goal state after:
a b : Ordinal.{u_1}
h : a ≤ b
c : Ordinal.{u_1}
hc : c < a
hx : c.toZFSet ∈ a.toZFSet
⊢ c.toZFSet ∈ b.toZFSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.refine_2.e_a
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 ^ succ ↑k * α' = (ω0 ^ ↑k * (ω0 * ↑↑n) + ω0 ^ ↑k * a'.repr + R) * α'

Tactic:
add_assoc,

Goal state after:
case succ.refine_2.e_a
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 ^ succ ↑k * α' = (ω0 ^ ↑k * (ω0 * ↑↑n) + (ω0 ^ ↑k * a'.repr + R)) * α'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case pos
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
hst : s = t
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
simp [hst]

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

Goal state before:
pp: basis : Basis
n : ℕ
h : n < List.length basis
⊢ (monomial basis n).toFun = basis[n]

Tactic:
let n' : Fin basis.length := ⟨n, h⟩
  conv_lhs => rw [show n = n'.val by simp [n']]
  convert! monomialRpow_toFun
  simp
  grind

Goal state after:
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:
by
    rw [eq_mk ms₁, eq_mk ms₂]
    simp [h]

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

Goal state before:
pp: case cons.cons.inl
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
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)

Tactic:
exact toFun_tendsto_zero_of_head_neg h_basis h

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

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ (f i).repr * ↑↑1 < ω ^ a.repr

Tactic:
PNat.one_coe,

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ (f i).repr * ↑1 < ω ^ a.repr
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous[inst✝¹, inst✝².toTopologicalSpace] (eval x ∘ F)
⊢ CompactSpace ↑(closure[inst✝¹] s)

Tactic:
have cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ ((↑) : closure s → ι)) K :=
    fun K hK ↦ (s_eqcont K hK).closure' <| show Continuous (K.domRestrict ∘ F) from
      continuous_pi fun ⟨x, hx⟩ ↦ this K hK x hx

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous[inst✝¹, inst✝².toTopologicalSpace] (eval x ∘ F)
cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
⊢ CompactSpace ↑(closure[inst✝¹] s)
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✝ : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 + p.2

Tactic:
let t₁ : TopologicalSpace E := .induced (B · ·) Pi.topologicalSpace

Goal state after:
𝕜 : 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✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 + p.2
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

Goal state after:
𝕜 : 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 𝕜 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 • p.2
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_7
E : Type u_8
F : Type u_9
inst✝⁷ : CommRing 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd 𝕜
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ -a

Tactic:
let t₁ : TopologicalSpace E := .induced (B · ·) Pi.topologicalSpace

Goal state after:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
inst✝⁷ : CommRing 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd 𝕜
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ -a
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
⊢ ∀ ⦃x : Set G⦄, x ⊆ a • ↑V → x ⊆ b • ↑V → x = ∅

Tactic:
intro x mem_aV mem_bV

Goal state after:
case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
⊢ x = ∅
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
ψ : PontryaginDual A
⊢ ψ = 1 → ψ ∈ V

Tactic:
rintro rfl _ _

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
x✝ : A
a✝ : x✝ ∈ Set.univ
⊢ 1 x✝ ∈ Circle.centeredArc (π / 2)
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
⊢ IsClosed[inst✝¹] (derivedSet A)

Tactic:
← derivedSet_closure,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
⊢ IsClosed[inst✝¹] (derivedSet (closure[inst✝¹] A))
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1

Tactic:
intro ⟨n, i⟩ _ ⟨m, j⟩ _ hne

Goal state after:
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)
a✝¹ : ⟨n, i⟩ ∈ univ
m : ℕ
j : ↑(E.I m)
a✝ : ⟨m, j⟩ ∈ univ
hne : ⟨n, i⟩ ≠ ⟨m, j⟩
⊢ Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ ⟨m, j⟩
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
this : ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
empty_union

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
this : ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ ∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
empty_union

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ∅ ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Tactic:
empty_union

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
this : ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = ↑E
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E

Tactic:
empty_union

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
this : ⋃ n, ⋃ j, openCell n ↑j = ↑E
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
inst✝ : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
empty_union

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
inst✝ : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ⋃ n, ⋃ j, openCell n ↑j = E