mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : ∀ (o : Ordinal.{u}), lfpApprox f x o = x
⊢ f x = x

pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x o = x

Tactic:
· specialize h 1
    rwa [← zero_add 1, lfpApprox_add_one f hx, lfpApprox_zero] at h

Goal state after:
case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x o = x
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Decidable (a ∈ l₂)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← Lists'.mem_cons]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Decidable (a ∈ l₂)
⊢ a ∈ b.cons' l₂ ↔ a ∈ Lists'.cons ⟨b✝, b⟩ l₂
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE

Tactic:
tfae_have 3 → 4
  | h => ⟨_, inter_subset_left, h.1, bddAbove_Iic.mono inter_subset_right, h.2⟩

Goal state after:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inl
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f 0 a

pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a

Tactic:
· exact H a

Goal state after:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a
Module: Mathlib.SetTheory.ZFC.Basic

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

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⟩
      exact ⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩

Goal state after:
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
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ ¬(match cmp o₁ o₂ with
        | Ordering.eq => cmp a b
        | Ordering.lt => cmp a (veblenWith f o₂ b)
        | Ordering.gt => cmp (veblenWith f o₁ a) b) =
        Ordering.gt ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Tactic:
aesop (add simp [not_lt_of_ge, lt_asymm])

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toZFSet.IsOrdinal

Tactic:
by
  refine ⟨fun x hx y hy ↦ ?_, fun {z y x} hz hy hx ↦ ?_⟩
  all_goals
    obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx
    obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy
  · exact toZFSet_mem_toZFSet_iff.2 (hb.trans ha)
  · obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hz
    exact toZFSet_mem_toZFSet_iff.2 (hc.trans hb)

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

Goal state before:
pp: case neg.refine_1
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 = ω * ω ^ (e.repr - 1)
⊢ ω * a'.repr + ↑m' < ω * ω ^ (e.repr - 1)

Tactic:
← this,

Goal state after:
case neg.refine_1
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 = ω * ω ^ (e.repr - 1)
⊢ ω * a'.repr + ↑m' < ω ^ e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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)
⊢ ω ∣ ω0

Tactic:
simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)

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

Goal state before:
pp: case h₁
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} := ⋯
R : Ordinal.{0} := ⋯
ω0 : Ordinal.{0} := ⋯
α' : Ordinal.{0} := ⋯
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 ^ ↑k * a'.repr + R < ω ^ (a0.repr * succ ↑k)

Tactic:
refine isPrincipal_add_omega0_opow _ ?_ Rl
      rw [opow_mul, opow_succ]
      gcongr
      exact No.snd'.repr_lt

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ClusterPt s (Filter.principal {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none})
n : ℕ
hn : s n = none
⊢ s (n + 1) = none

Tactic:
clusterPt_principal_iff

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
⊢ s (n + 1) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ CompleteSpace (Stream'.Seq α)

Tactic:
suffices IsClosed (X := Stream' (Option α)) {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none} by
    exact this.completeSpace_coe
  rw [isClosed_iff_clusterPt]
  intro s hs n hn
  rw [clusterPt_principal_iff] at hs
  obtain ⟨t, hts, ht⟩ := hs (Metric.ball s ((1 / 2 : ℝ) ^ (n + 1)))
    (Metric.ball_mem_nhds _ (by positivity))
  simp only [Metric.ball, Set.mem_ofPred_eq] at hts
  rw [← PiNat.apply_eq_of_dist_lt hts (by simp)] at hn
  rw [← PiNat.apply_eq_of_dist_lt hts (by rfl)]
  exact ht hn

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

Goal state before:
pp: γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
⊢ x = y

Tactic:
by
  apply Seq.FriendlyOperationClass.eq_of_bisim (op := op) motive base
  peel step with x y ih h
  obtain h | ⟨exp, coef, c, x', y', rfl, rfl, h_next⟩ := h
  · simp [h]
  right
  use (exp, coef), x', y', c
  simpa [cons]

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

Goal state before:
pp: case h1
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t1.unit = List.length (left ++ right)

Tactic:
simpa [t2']

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

Goal state before:
pp: case h2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t2'.unit = List.length (left ++ right)

Tactic:
simpa [t2']

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

Goal state before:
pp: case h_coef2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.coef ≠ 0

Tactic:
simpa [t2']

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

Goal state before:
pp: case h_lt
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.unit < t2'.unit

Tactic:
simpa [t2']

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

Goal state before:
pp: case h1
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t2'.unit = List.length (left ++ right)

Tactic:
simpa [t2']

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

Goal state before:
pp: case h2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t1.unit = List.length (left ++ right)

Tactic:
simpa [t2']

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

Goal state before:
pp: case h_coef2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.coef ≠ 0

Tactic:
simpa [t2']

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

Goal state before:
pp: case h_lt
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.unit < t1.unit

Tactic:
simpa [t2']

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
h : (Multiseries.cons exp coef tl).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
generalize h_ms : Multiseries.cons exp coef tl = ms at h
  cases h with
  | nil => simp at h_ms
  | cons h_trimmed h_ne_zero =>
    simp at h_ms
    grind

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

Goal state before:
pp: case hyp.inr.inr
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.toFun =ᶠ[atTop] 0 ∧ ms.seq = Multiseries.nil ∨
    ∃ basis_hd_1 f basis_tl_1 exp coef,
      (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
        Majorized f basis_hd_1 exp ∧
          ∃ x,
            ((mk x (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h : basis_hd_1 = basis_hd ∧ basis_tl_1 = basis_tl),
                  motive (⋯ ▸ mk x (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f

Tactic:
· refine .inr ⟨basis_hd, ms.toFun, basis_tl, exp, coef, by simpa, ‹_›, tl, ?_⟩
      simp
      grind

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

Goal state before:
pp: case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ n.factorization z = q • f z

Tactic:
smul_eq_mul,

Goal state after:
case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ n.factorization z = q * f z
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✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
      ← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]
  rfl

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

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
⊢ (ConcreteCategory.hom (quotientMap f Y)) (x (preimage f Y)) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) (x (preimage f X)))

Tactic:
← this,

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
⊢ (ConcreteCategory.hom (quotientMap f Y))
      ((ConcreteCategory.hom
          ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
        (x (preimage f X))) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) (x (preimage f X)))
Module: Mathlib.Topology.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
⊢ IsClosed ↑(unitary R)

Tactic:
let f (u : R) : R × R := (star u * u, u * star u)
  have hf : f ⁻¹' {(1, 1)} = unitary R := by ext u; simp [f, Unitary.mem_iff]
  rw [← hf]
  exact isClosed_singleton.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : cell C m
hj : j ∈ J m
hxj : x ∈ openCell m j
this : x ∈ ↑E
hj' : ¬j ∈ E.I m
⊢ False

Tactic:
exact E.disjoint_openCell_subcomplex_of_not_mem hj' |>.notMem_of_mem_left hxj this

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

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

Tactic:
simp only [disjoint_empty, implies_true]

Goal state after:
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 : Finite C
h : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell C n)
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
⊢ _root_.Finite ((n : ℕ) × cell C n)

Tactic:
simp only [Filter.eventually_atTop] at h

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
h : ∃ a, ∀ (b : ℕ), a ≤ b → IsEmpty (cell C b)
⊢ _root_.Finite ((n : ℕ) × cell C n)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : ↑(π C fun x ↦ x ∈ s) → ↥s → Bool := fun x j ↦ ↑x ↑j
⊢ Function.Injective f

Tactic:
intro ⟨_, x, hx, rfl⟩ ⟨_, y, hy, rfl⟩ h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : ↑(π C fun x ↦ x ∈ s) → ↥s → Bool := fun x j ↦ ↑x ↑j
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h : f ⟨Proj (fun x ↦ x ∈ s) x, ⋯⟩ = f ⟨Proj (fun x ↦ x ∈ s) y, ⋯⟩
⊢ ⟨Proj (fun x ↦ x ∈ s) x, ⋯⟩ = ⟨Proj (fun x ↦ x ∈ s) y, ⋯⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x ↦ x ∈ s)
h : (Finsupp.onFinset Finset.univ f.toFun ⋯) x = 0
⊢ 0 = f x

Tactic:
exact h.symm

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
I J : (n : ℕ) → Set (cell C n)
hIJ : ⋃ n, ⋃ j, openCell n ↑j = ⋃ n, ⋃ j, openCell n ↑j
⊢ ⋃ n, ⋃ j, openCell n ↑j = ⋃ n, ⋃ j, openCell n ↑j

Tactic:
hIJ

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
X✝ Y✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ProjRestricts C ⋯ = ProjRestricts C ⋯ ∘ ProjRestricts C ⋯

Tactic:
rw [projRestricts_eq_comp]

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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
⊢ ord I (↑↑l).head! = o

Tactic:
have hm := l.prop.2

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 : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
⊢ ord I (↑↑l).head! = o
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
⊢ IsCompactSystem S

Tactic:
intro C hC
  contrapose!
  exact h C hC

Goal state after: