mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
this✝ : NeZero (p - 1)
this : Nat.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
⊢ p - 1 ≤ Nat.card ↥(rootsOfUnity (p - 1) (ZMod p))

Tactic:
rw [this]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
this✝ : NeZero (p - 1)
this : Nat.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
⊢ p - 1 ≤ Nat.card ↥⊤
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 : ℕ
x y : 𝕎 k
⊢ peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] =
    (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:
peval_polyOfInterest

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
⊢ (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i) =
    (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)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
zero_right

Goal state after:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ [(0, o)] = [(0, o)]
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_1
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b 0))

Tactic:
zero_right

Goal state after:
case refine_1
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst [])
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.lookupFinsupp e = c

Tactic:
lookupFinsupp_apply,

Goal state after:
b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (AList.lookup e { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }).getD 0 = c
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
⊢ IsOpen[inst✝²] {a}

Tactic:
by_cases ha' : IsMax a

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ IsOpen[inst✝²] {a}

case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ IsOpen[inst✝²] {a}
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
⊢ Acc (fun x1 x2 ↦ x1 ∈ x2) (mk γ C)

Tactic:
have H := ha.trans hc.symm

Goal state after:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H✝ : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
H : ((mk α A).Func a).Equiv (mk γ C)
⊢ Acc (fun x1 x2 ↦ x1 ∈ x2) (mk γ C)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u_1}
H : {x} = {y}
⊢ x = y

Tactic:
let := congr_arg sUnion H
  rwa [sUnion_singleton, sUnion_singleton] at this

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ (∃ i, f i = ⟦y⟧) → ⟦y⟧ ∈ range f

Tactic:
rintro ⟨z, hz⟩
      use equivShrink α z
      simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)

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

Goal state before:
pp: α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ ((mk α✝ A✝).Func w✝).rank < (mk α✝ A✝).rank

Tactic:
← succ_le_iff

Goal state after:
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ succ ((mk α✝ A✝).Func w✝).rank ≤ (mk α✝ A✝).rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ o ≤ (veblen o a).invVeblen₁

Tactic:
rw [← mem_range_veblen_iff_le_invVeblen₁]
    obtain rfl | ho := eq_zero_or_pos o
    · simp
    · rw [← veblen_zero_apply, veblen_veblen_of_lt ho]
      simp

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

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_

Tactic:
mem_range_gamma,

Goal state after:
case mp
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → o = 0 ∨ veblen o 0 = o
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩

Goal state after:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ ⋃₀ x

Tactic:
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩

Goal state after:
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x
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:
_zsmul_neg_trick

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

Goal state before:
pp: case refine_2.inl
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
h : w.IsOrdinal
hw : w ∈ insert w w
⊢ y ∈ w

pp: case refine_2.inr
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw✝ : w ∈ insert x x
hw : w ∈ x
⊢ y ∈ w

Tactic:
exacts [h.mem_trans hyz hzw, h.mem_trans' hyz hzw hw]

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

Goal state before:
pp: o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = x

Tactic:
induction x using Quotient.ind

Goal state after:
case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
⊢ ⟦a✝⟧ ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = ⟦a✝⟧
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_1
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x ∈ Set.range toZFSet

Tactic:
rw [← h.toZFSet_rank_eq]

Goal state after:
case refine_1
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x.rank.toZFSet ∈ Set.range toZFSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.refine_2
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'

Tactic:
rw [this]

Goal state after:
case neg.refine_2
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ ω ^ 1 * ω ^ (e.repr - 1) * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r : ℝ
⊢ Majorized (f ^ r) hd 0

Tactic:
by
  intro exp h_exp
  apply pow_isLittleO_pow_of_log
  · exact h_basis.tail.eventually_pos.mono fun _ h ↦ h _ hf
  · exact h_basis.tendsto_atTop (by simp)
  · grind [WellFormedBasis, List.pairwise_cons]
  · exact h_exp

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

Goal state before:
pp: hd : ℝ
tl : UnitMonomial
h_hd : hd = 0
h_tl : tl.FirstNonzeroIsPos
⊢ FirstNonzeroIsPos (hd :: tl)

Tactic:
by
  simp [h_hd, h_tl]

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

Goal state before:
pp: hd : ℝ
tl : UnitMonomial
h_hd : hd = 0
h_tl : tl.FirstNonzeroIsNeg
⊢ FirstNonzeroIsNeg (hd :: tl)

Tactic:
by
  simp [h_hd, h_tl]

Goal state after:
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).destruct = some (exp, coef, tl)

Tactic:
simp [destruct, cons]

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

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
suffices h_log : Tendsto (Real.log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl))
      atTop atTop by
    apply Filter.Tendsto.congr' _ (Real.tendsto_exp_atTop.comp h_log)
    apply (toFun_pos (m := (exps_hd :: exps_tl)) h_basis).mono
    intro x hx
    simp only [Function.comp_apply]
    exact Real.exp_log hx

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
⊢ Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.nil
exps_hd : ℝ
exps_tl : List ℝ
h_allZero : AllZero (exps_hd :: exps_tl)
⊢ Tendsto (toFun (exps_hd :: exps_tl) []) atTop (𝓝 1)

Tactic:
eta_expand
      simp [toFun]

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

Goal state before:
pp: x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1

Tactic:
exact Nat.ne_of_beq_eq_false h

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

Goal state before:
pp: a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
by
  refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
  rw [h.1, Int.cast_negOfNat] at hb
  rcases eq_or_ne b 0 with rfl | hb₀
  · simp_all
  · refine absurd hb (ne_of_lt ?_)
    exact lt_of_le_of_lt (by simp) (mul_self_pos.mpr hb₀)

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

Goal state before:
pp: a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
by
  refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
  rw [h.1, Int.cast_negOfNat] at hb
  rcases eq_or_ne b 0 with rfl | hb₀
  · simp_all
  · refine absurd hb (ne_of_lt ?_)
    exact lt_of_le_of_lt (by simp) (mul_self_pos.mpr hb₀)

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

Goal state before:
pp: a b m : ℕ
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m

Tactic:
pow_add,

Goal state after:
a b m : ℕ
⊢ a ^ (2 * b) * a ^ 1 % m = a ^ b % m * (a ^ b % m * a % m) % m
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m : ℕ
⊢ a ^ (b + b) * a ^ 1 % m = a ^ b % m * (a ^ b % m * a % m) % m

Tactic:
pow_add,

Goal state after:
a b m : ℕ
⊢ a ^ b * a ^ b * a ^ 1 % m = a ^ b % m * (a ^ b % m * a % m) % m
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: case mk.mk
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
⊢ (if val✝ < val✝¹ then val✝¹ - val✝ else 1) = val✝¹ - 1 - val✝ + 1

Tactic:
split_ifs <;> lia

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∈ xs
⊢ x = y

Tactic:
rw [List.mem_iff_getElem?] at hx hy

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : ∃ i, xs[i]? = some x
hy : ∃ i, xs[i]? = some y
⊢ x = y
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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
UniformSpace.comap_comap,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap F (UniformSpace.comap (⋃₀ 𝔖).domRestrict (Pi.uniformSpace fun i ↦ α)) =
    ⨅ K ∈ 𝔖, UniformSpace.comap F (UniformSpace.comap K.domRestrict (Pi.uniformSpace fun i ↦ α))
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g ↦ g • 1
⊢ IsOpenMap ⇑f

Tactic:
rw [this]

Goal state after:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g ↦ g • 1
⊢ IsOpenMap fun g ↦ g • 1
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
this : c ^ (k + 1) • w ∈ c • V
⊢ c ^ k • w ∈ V

Tactic:
pow_add,

Goal state after:
𝕜₁ : 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
this : (c ^ k * c ^ 1) • w ∈ c • V
⊢ c ^ k • w ∈ V
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)
this : -1 + ↑this✝.unit⁻¹ = -↑this✝.unit⁻¹ * x
⊢ -1 + ↑this✝.unit⁻¹ ∈ I ^ n

Tactic:
rw [this]

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)
this : -1 + ↑this✝.unit⁻¹ = -↑this✝.unit⁻¹ * x
⊢ -↑this✝.unit⁻¹ * x ∈ I ^ n
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
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✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ -π < 2 * (↑x).arg ∧ 2 * (↑x).arg < π

Tactic:
← abs_lt,

Goal state after:
case refine_1
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✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ |2 * (↑x).arg| < π
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
Z : Type v'
inst✝ : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[TopologicalSpace.coinduced (⇑f) inferInstance, inst✝] g ↔
    Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)

Tactic:
rw [continuous_coinduced_dom]; simp [equiv, Equiv.refl]

Goal state after:
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:
← Set.image_comp

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 y ∈ Proj J ∘ Proj K '' C
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
this : eval (π C J) l = 0
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Tactic:
rw [this]

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
this : eval (π C J) l = 0
⊢ 0 ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x ↦ x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
⊢ ⇑(πJ C K) '' Set.range (eval (π C fun x ↦ x ∈ K)) ⊆ Set.range (Products.eval C)

Tactic:
rintro l ⟨y, ⟨m, rfl⟩, rfl⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x ↦ x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
m : { l // Products.isGood (π C fun x ↦ x ∈ K) l }
⊢ (πJ C K) (eval (π C fun x ↦ x ∈ K) m) ∈ Set.range (Products.eval C)
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (πs C o₂) ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)) = (πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)

Tactic:
← LocallyConstant.coe_inj,

Goal state after:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ ⇑((πs C o₂) ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))) =
    ⇑((πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))
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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) l) = eval (π C fun x ↦ ord I x < o₂) l

Tactic:
← LocallyConstant.coe_inj,

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ ⇑((πs' C h) (eval (π C fun x ↦ ord I x < o₁) l)) = ⇑(eval (π C fun x ↦ ord I x < o₂) l)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ SumEval C ho ∘ Sum.inl = ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o))) ∘ eval (π C fun x ↦ ord I x < o)

Tactic:
by
  ext l
  dsimp [SumEval]
  rw [← Products.eval_πs C (Products.prop_of_isGood _ _ l.prop)]
  simp [eval]

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
⊢ SwapTrue o x (term I ho) = true

Tactic:
by
  simp only [SwapTrue, ord_term_aux, ite_true]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀ x ∈ C' C ho, x (term I ho) = false

Tactic:
rintro x ⟨_, y, _, rfl⟩
  simp only [Proj, ord_term_aux, lt_self_iff_false, ite_false]

Goal state after: