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

Goal state before:
pp: α : Type u_1
a y : Lists α
l : Lists' α true
⊢ a ∈ cons y l ↔ a ~ y ∨ a ∈ l

Tactic:
simp [mem_def, or_and_right, exists_or]

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
a : Ordinal.{u}
⊢ lfpApprox f x a ≤ lfpApprox g x a

Tactic:
induction a using WellFoundedLT.induction with | ind i IH
   =>  _ 

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ lfpApprox f x i ≤ lfpApprox g x i
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ l ⊆ l

Tactic:
rw [← Lists'.of_toList l]

Goal state after:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
a : Ordinal.{u}
⊢ lfpApprox f x₁ a ≤ lfpApprox f x₂ a

Tactic:
induction a using WellFoundedLT.induction with | ind i IH
   =>  _ 

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ Monotone (lfpApprox f)

Tactic:
by
  intro x₁ x₂ h a
  induction a using WellFoundedLT.induction with | ind i IH
  rw [lfpApprox, lfpApprox]
  exact sup_le_sup h <| iSup₂_mono fun j hj ↦ f.mono (IH j hj)

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries.keys.toFinset = (map Prod.fst (CNF b o)).toFinset

Tactic:
simp [List.keys]

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

Goal state before:
pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ foldr (fun p r ↦ b ^ p * (single e x + f) p + r) 0 (e :: f.support.sort fun x1 x2 ↦ x1 ≥ x2) = b ^ e * x + eval b f

Tactic:
simp only [add_apply, foldr_cons, single_eq_same, hf, add_zero, add_right_inj]

Goal state after:
case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ foldr (fun p r ↦ b ^ p * ((single e x) p + f p) + r) 0 (f.support.sort fun x1 x2 ↦ x1 ≥ x2) = eval b f
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 α
ha : a ∈ frontier s
⊢ IsSuccLimit a

Tactic:
← isOpen_singleton_iff.not_left

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : a ∈ frontier s
⊢ ¬IsOpen[inst✝³] {a}
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
sUnion_singleton

Goal state after:
x y : ZFSet.{u_1}
H : {x} = {y}
this : x = y
⊢ x = y
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : PSet.{u_1}
⊢ max (succ x.rank) y.rank ≤ (insert x y).rank

Tactic:
· apply max_le
    · exact (rank_lt_of_mem (mem_insert x y)).succ_le
    · exact rank_mono (subset_iff.2 fun z => mem_insert_of_mem x)

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

Goal state before:
pp: s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ x ∈ ↑(mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x))) ↔ x ∈ s

Tactic:
rw [SetLike.mem_coe, ← mk_out x, mk_mem_iff, mk_out]

Goal state after:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)) ↔ x ∈ s
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'⟩
  exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)

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

Goal state before:
pp: case mp
x y : ZFSet.{u}
⊢ x.IsOrdinal → y.IsOrdinal → x ⊆ y → x = y ∨ x ∈ y

Tactic:
refine Sym2.GameAdd.recursion mem_wf ?_ x y

Goal state after:
case mp
x y : ZFSet.{u}
⊢ ∀ (a₁ b₁ : ZFSet.{u}),
    (∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(a₁, b₁) →
          a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂) →
      a₁.IsOrdinal → b₁.IsOrdinal → a₁ ⊆ b₁ → a₁ = b₁ ∨ a₁ ∈ b₁
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ V_ b

Tactic:
rw [vonNeumann]; aesop

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

Goal state before:
pp: case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ ℵ₀ ≤ #↑(Set.Iio o)

Tactic:
rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]

Goal state after:
case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ Ordinal.omega0 ≤ o
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ n, dist s t = 2⁻¹ ^ n

Tactic:
rw [Subtype.dist_eq, PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h)]

Goal state after:
α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ n, (1 / 2) ^ PiNat.firstDiff ↑s ↑t = 2⁻¹ ^ n
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.a1
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ 1 < ↑m + 1

pp: case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω

Tactic:
· simpa [Nat.one_le_iff_ne_zero]

Goal state after:
case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω
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

pp: case neg
α : 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:
case neg
α : 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
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o a : Ordinal.{u_1}
h : a < o * ω
⊢ ∃ i, a < o * ↑i + o

Tactic:
by
  obtain ⟨i, hi, h'⟩ := (lt_mul_iff_of_isSuccLimit isSuccLimit_omega0).1 h
  obtain ⟨i, rfl⟩ := lt_omega0.1 hi
  exact ⟨i, h'.trans_le le_self_add⟩

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 : exps_hd ≠ 0
⊢ toLogFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd

Tactic:
by
  simp only [toLogFun_cons]
  apply IsEquivalent.refl.add_isLittleO
  apply IsLittleO.const_mul_right' (isUnit_iff_ne_zero.mpr h_nonzero)
  have hlo : ∀ b ∈ basis_tl, (Real.log ∘ b) =o[atTop] (Real.log ∘ basis_hd) :=
    fun b hb => h_basis.tail_isLittleO_head hb
  clear h_basis
  induction exps_tl generalizing basis_tl with
  | nil =>
    simp only [toLogFun_nil]
    exact Asymptotics.isLittleO_zero _ _
  | cons e es ih =>
    cases basis_tl with
    | nil =>
      simp only [toLogFun_nil_basis]
      exact Asymptotics.isLittleO_zero _ _
    | cons b bs =>
      exact (IsLittleO.const_mul_left (hlo b (by simp)) e).add (ih (by grind))

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 : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atBot
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)

Tactic:
have hmono := Real.tendsto_exp_atBot.comp h_log

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atBot
hmono : Tendsto (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)
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
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
rw [h_eq]

Goal state after:
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
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun exps_tl basis_tl) atTop atTop
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 ∧ FirstNonzeroIsNeg exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)

Tactic:
rw [h_eq]

Goal state after:
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 ∧ FirstNonzeroIsNeg exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun exps_tl basis_tl) atTop (𝓝 0)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 1)

Tactic:
rw [h_eq]

Goal state after:
case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun exps_tl basis_tl) atTop (𝓝 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
x : ℝ
hx : 0 < basis_hd x
⊢ basis_hd x ^ exp2 / basis_hd x ^ exp1 * (toFun m2 basis_tl x * (toFun m1 basis_tl x)⁻¹) =
    basis_hd x ^ exp2 * toFun m2 basis_tl x / (basis_hd x ^ exp1 * toFun m1 basis_tl x)

Tactic:
field

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
hd : α
u v : Stream'.Seq α
ih : dist u v ≤ 2⁻¹ ^ n
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ 2⁻¹ * dist u v ≤ 2⁻¹ ^ (n + 1)

Tactic:
grw [ih, pow_succ']

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

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ 0 ≤ x

Tactic:
simp only [hx_eq, invOf_eq_inv]

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ 0 ≤ ↑x_num * (↑x_den)⁻¹
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
⊢ IsNNRat (√x) sn sd

Tactic:
by
  obtain ⟨_, rfl⟩ := h
  refine ⟨?_, ?out⟩
  · apply invertibleOfNonzero
    rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]
    exact Invertible.ne_zero _
  · simp [← hn, ← hd, Real.sqrt_mul (mul_self_nonneg ↑sn)]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 0 = ∅

Tactic:
by simp only [Icc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 1 = {1}

Tactic:
by simp only [Icc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 2 = {1, 2}

Tactic:
by simp only [Icc_ofNat_ofNat]

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

Goal state before:
pp: case e_opt
α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m

Tactic:
induction m with

Goal state after:
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)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F

Tactic:
by
  rw [eq_univ_iff_forall] at 𝔖_covers
  -- This obviously follows from the previous lemma, we formalize it by going through the
  -- isomorphism of uniform spaces between `(⋃₀ 𝔖) → α` and `X → α`.
  let φ : ((⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (β := fun _ ↦ α)
    (Equiv.subtypeUnivEquiv 𝔖_covers)
  rw [EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,
      show domRestrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl]
  exact ⟨fun H ↦ φ.isUniformInducing.comp H, fun H ↦ φ.symm.isUniformInducing.comp H⟩

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

Goal state before:
pp: G : GrpCat
⊢ Mono (eta G) ↔ Group.ResiduallyFinite ↑G

Tactic:
GrpCat.mono_iff_injective,

Goal state after:
G : GrpCat
⊢ Function.Injective ⇑(ConcreteCategory.hom (eta G)) ↔ Group.ResiduallyFinite ↑G
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: 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
⊢ DiscreteTopology (PontryaginDual A)

Tactic:
by
  let V : Set (PontryaginDual A) := {ψ | Set.MapsTo ψ Set.univ (Circle.centeredArc (π / 2))}
  have hVopen : IsOpen V := by
    dsimp only [V]
    exact isOpen_induced (ContinuousMap.isOpen_setOfPred_mapsTo isCompact_univ
      (Circle.isOpen_centeredArc (π / 2)))
  have hVeq : V = ({1} : Set (PontryaginDual A)) := by
    ext ψ
    rw [Set.mem_singleton_iff]
    refine ⟨fun hψ ↦ ?_, ?_⟩
    · ext1 a
      refine Circle.eq_one_of_forall_pow_mem_centeredArc_pi_div_two fun n hn ↦ ?_
      simpa using hψ (Set.mem_univ (a ^ n))
    · rintro rfl _ _
      rw [Circle.mem_centeredArc (by linarith [pi_pos])]
      simp [pi_pos]
  exact discreteTopology_of_isOpen_singleton_one (by simpa [hVeq] using hVopen)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x y : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 y) ![], ↑(map 0 x) ![]}
⊢ ∃ x, cellFrontier 1 e = closedCell 0 x

Tactic:
obtain rfl : x = y := RelCWComplex.injective_map_zero C <| (hxy ▸ h) (by simp) (by simp)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 x) ![]}
⊢ ∃ x, cellFrontier 1 e = closedCell 0 x
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
⊢ ∀ (n : ℕ) (i : ↑(E.I n)),
    ∃ I, MapsTo (↑(map n ↑i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m ↑j) '' closedBall 0 1)

Tactic:
by
    intro n i
    rcases cellFrontier_subset_finite_openCell (C := C) n i with ⟨J, hJ⟩
    use fun m ↦ Finset.preimage (J m) Subtype.val Subtype.val_injective.injOn
    rw [mapsTo_iff_image_subset]
    intro x hx
    specialize hJ hx
    simp_rw [iUnion_coe_set, mem_union, mem_iUnion, Finset.mem_preimage, exists_prop,
      Decidable.or_iff_not_imp_left] at hJ ⊢
    intro h
    specialize hJ h
    obtain ⟨m, hmn, j, hj, hxj⟩ := hJ
    suffices j ∈ E.I m from ⟨m, hmn, j, this, hj, openCell_subset_closedCell _ _ hxj⟩
    have : x ∈ (E : Set X) := E.cellFrontier_subset_of_mem i.2 hx
    by_contra hj'
    exact E.disjoint_openCell_subcomplex_of_not_mem hj' |>.notMem_of_mem_left hxj this

Goal state after:
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
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
x✝ : 0 < n
j : cell C n
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
by_cases hj : j ∈ E.I n

Goal state after:
case pos
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
x✝ : 0 < n
j : cell C n
hj : j ∈ E.I n
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

case neg
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
x✝ : 0 < n
j : cell C n
hj : j ∉ E.I n
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp.left
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic A

Tactic:
filter_upwards [hG] with _

Goal state after:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ A
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp.right
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic B

Tactic:
filter_upwards [hG] with _

Goal state after:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ B
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
⊢ X.str F ∈ cl A

Tactic:
let C0 : ssu := { Z | ∃ B ∈ F, X.str ⁻¹' B = Z }

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
⊢ X.str F ∈ cl A
Module: Mathlib.Topology.CWComplex.Classical.Basic

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

Tactic:
simpa only [empty_union] using CWComplex.union'

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

Goal state before:
pp: case h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ ∈ F ∧ Set.univ = basic Set.univ

Tactic:
refine ⟨Filter.univ_sets _, ?_⟩

Goal state after:
case h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ = basic Set.univ
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ Continuous fun c i ↦ if J i then c i else false

Tactic:
apply continuous_pi

Goal state after:
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ ∀ (i : I), Continuous fun a ↦ if J i then a i else false
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Continuous fun f i ↦ if ord I i = o then true else f i

Tactic:
apply continuous_pi

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ ∀ (i : I), Continuous fun a ↦ if ord I i = o then true else a i