mathlib-initiative/mathlib-tactics huggingface dataset:
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 * α' + R) * α'

Tactic:
mul_add (ω0 ^ (k : Ordinal)),

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.Majorized

Goal state before:
pp: f g basis_hd : ℝ → ℝ
exp : ℝ
hf : Majorized f basis_hd exp
hg : g =O[atTop] fun x ↦ 1
⊢ Majorized (f * g) basis_hd exp

Tactic:
by
  intro exp h_exp
  convert! IsLittleO.mul_isBigO (hf _ h_exp) hg using 1
  simp
  rfl

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 : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ s (n + 1) = none

Tactic:
rw [← PiNat.apply_eq_of_dist_lt hts (by rfl)]

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 : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ t (n + 1) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ 2⁻¹ ^ PiNat.firstDiff ↑(Seq.cons x s) ↑(Seq.cons x t) = 2⁻¹ ^ (PiNat.firstDiff ↑s ↑t + 1)

Tactic:
congr

Goal state after:
case neg.e_a
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ PiNat.firstDiff ↑(Seq.cons x s) ↑(Seq.cons x t) = PiNat.firstDiff ↑s ↑t + 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.some
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ op c (f b') =
    op c
      (match F b' with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))

Tactic:
congr

Goal state after:
case h.some.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ f b' =
    match F b' with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
hd : α
x : Stream'.Seq α
⊢ ∀ (t : Stream'.Seq α), 2⁻¹ * dist x t ≤ dist x t

Tactic:
y

Goal state after:
α : Type u_1
hd : α
x y : Stream'.Seq α
⊢ 2⁻¹ * dist x y ≤ dist x y
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
x : Stream'.Seq α
⊢ ∀ (t : Stream'.Seq α), dist (op (Seq.cons hd x)).tail (op (Seq.cons hd t)).tail ≤ dist x t

Tactic:
y

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
x y : Stream'.Seq α
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ one = cons 0 MultiseriesExpansion.one nil

Tactic:
by
  simp [Multiseries.one, Multiseries.const_def, MultiseriesExpansion.one]

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

Goal state before:
pp: case cons.zero
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (mk (Multiseries.monomialRpow basis_hd basis_tl (↑0) r) ((basis_hd :: basis_tl)[↑0] ^ r)).Approximates

Tactic:
simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, Multiseries.monomialRpow,
        List.getElem_cons_zero]

Goal state after:
case cons.zero
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (mk (Multiseries.cons r one Multiseries.nil) (basis_hd ^ r)).Approximates
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case succ
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ (n + 1)
T : Option α → Option (α × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        (T s.head)
h_head : s.head = t.head
hs :
  (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (T s.head)
ht :
  (op t).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' t.tail))
      (T t.head)
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ (n + 1)

Tactic:
cases hT_head : T s.head with
    | none =>
      simp only [hT_head, Option.map_none, ← h_head] at hs ht
      simp [hs, ht, destruct_eq_none]
    | some v =>
      obtain ⟨hd, op', h_next⟩ := v
      simp only [hT_head, Option.map_some, ← h_head] at hs ht
      simp only [destruct_eq_cons hs, destruct_eq_cons ht, dist_cons_cons, pow_succ', inv_pos,
        Nat.ofNat_pos, mul_le_mul_iff_right₀, ge_iff_le]
      apply ih h_next
      simpa [dist_eq_half_of_head h_head, pow_succ'] using hn

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

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
h_neg : (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).leadingExp < 0
h_approx : (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).Approximates
⊢ Tendsto (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).toFun atTop (𝓝 0)

Tactic:
· obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
    simp only [leadingExp_def, mk_seq, Multiseries.leadingExp_cons, WithBot.coe_lt_zero] at h_neg
    exact Majorized.tendsto_zero_of_neg h_neg h_maj

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
⊢ (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)

Tactic:
refine ⟨h4, h5, fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (h6 H.fst)))⟩

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).oadd 1 0).repr < ω ^ a.repr
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ √x = ↑ny

Tactic:
simp [h.out, ← hy]

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

Goal state before:
pp: x : ℝ≥0
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ sqrt x = ↑ny

Tactic:
simp [h.out, ← hy]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
⊢ ∀ ⦃a₂ : α⦄, List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) a₂ → x = a₂

Tactic:
y

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
⊢ List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y → x = y
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 : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = xs[j]?

Tactic:
congr

Goal state after:
case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i = j
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 ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing F

Tactic:
EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsInducing ((⋃₀ 𝔖).domRestrict ∘ F) ↔ IsInducing F
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ (DenseRange fun x_1 ↦ x ^ x_1) ↔ DenseRange fun x_1 ↦ x ^ x_1

Tactic:
simp only [DenseRange, dense_iff_closure_eq, closure_range_zpow_eq_pow]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).topologicalClosure = (Submonoid.closure s).topologicalClosure

Tactic:
refine le_antisymm ?_ (closure_mono <| Subgroup.le_closure_toSubmonoid _)
  refine Submonoid.topologicalClosure_minimal _ ?_ isClosed_closure
  rw [Subgroup.closure_toSubmonoid, Submonoid.closure_le]
  refine union_subset (Submonoid.subset_closure.trans subset_closure) fun x hx ↦ ?_
  refine closure_mono (Submonoid.powers_le.2 (Submonoid.subset_closure <| Set.mem_inv.1 hx)) ?_
  rw [Submonoid.coe_powers, ← closure_range_zpow_eq_pow, ← Subgroup.coe_zpowers,
    ← Subgroup.topologicalClosure_coe, SetLike.mem_coe, ← inv_mem_iff]
  exact subset_closure <| Subgroup.mem_zpowers _

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
⊢ ({1}.indicator fun x ↦ e) ⋆[L] f = f

Tactic:
by
  classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]

Goal state after:
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
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ ∀ (i : F),
    Continuous[TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace, inst✝⁶] fun a ↦
      ((fun x1 x2 ↦ (B x1) x2) ∘ fun a ↦ -a) a i

Tactic:
Function.comp_apply,

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
this : B.IsWeak
⊢ ∀ (i : F), Continuous[TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace, inst✝⁶] fun a ↦ (B (-a)) i
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx hy : x ∈ Metric.sphere 0 1
h :
  (ConcreteCategory.hom (diskBoundaryInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (diskBoundaryInclusion n)) { down := ⟨x, hy⟩ }
⊢ { down := ⟨x, hx⟩ } = { down := ⟨x, hy⟩ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx hy : x ∈ Metric.ball 0 1
h :
  (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hy⟩ }
⊢ { down := ⟨x, hx⟩ } = { down := ⟨x, hy⟩ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (⇑(map C h) ∘ ⇑(π_app C (Membership.mem K))) x ∈ {↑a (op J)}

Tactic:
Function.comp_apply,

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (map C h) ((π_app C (Membership.mem K)) x) ∈ {↑a (op J)}
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x : cell C 0
⊢ ∀ ⦃a₂ : cell C 0⦄, closedCell 0 x = closedCell 0 a₂ → x = a₂

Tactic:
y

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
⊢ closedCell 0 x = closedCell 0 y → x = y
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x : cell C 0
⊢ ∀ ⦃a₂ : cell C 0⦄, openCell 0 x = openCell 0 a₂ → x = a₂

Tactic:
y

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
⊢ openCell 0 x = openCell 0 y → x = y
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
x : I → Bool
h : x ∈ π C J
⊢ x ∈ π (π C K) J

Tactic:
obtain ⟨y, hy, rfl⟩ := h
    dsimp [π]
    rw [← Set.image_comp]
    refine ⟨y, hy, ?_⟩
    rw [proj_comp_of_subset J K h]

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✝
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } =
    CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
      ({ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ }.comp { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ })

Tactic:
congr

Goal state after:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
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 ⋯ =
    ⇑{ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } ∘ ⇑{ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
⊢ isGood {fun x ↦ false} nil

Tactic:
intro h
  simp [Products.eval, Products.nil] at h

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

Goal state before:
pp: case h
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 h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x ↦ ord I x < o₂) ∧
    (π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:
refine ⟨?_, ?_⟩

Goal state after:
case h.refine_1
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 h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x ↦ ord I x < o₂)

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.Successor

Goal state before:
pp: case refine_3.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₁ : x ∈ C1 C ho
hx₁' : ↑(ProjRestrict C (fun x ↦ ord I x < o) ⟨x, hx⟩) ∈ π (C1 C ho) fun x ↦ ord I x < o
⊢ f
      ({ toFun := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩, continuous_toFun := h₁ }
        ⟨↑(ProjRestrict C (fun x ↦ ord I x < o) ⟨x, hx⟩), hx₁'⟩) =
    f ⟨x, hx⟩

Tactic:
congr

Goal state after:
case refine_3.inr.e_6
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := ⋯
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := ⋯
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₁ : x ∈ C1 C ho
hx₁' : ↑(ProjRestrict C (fun x ↦ ord I x < o) ⟨x, hx⟩) ∈ π (C1 C ho) fun x ↦ ord I x < o
⊢ { toFun := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩, continuous_toFun := h₁ }
      ⟨↑(ProjRestrict C (fun x ↦ ord I x < o) ⟨x, hx⟩), hx₁'⟩ =
    ⟨x, hx⟩
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I✝¹ : (n : ℕ) → Set (cell C n)
closed'✝¹ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
F : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] F
hF : D ∪ ⋃ n, ⋃ j, openCell n ↑j = F
h :
  (fun E ↦ E.carrier) { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    (fun E ↦ E.carrier) { carrier := F, I := I✝, closed' := closed'✝, union' := hF }
⊢ { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    { carrier := F, I := I✝, closed' := closed'✝, union' := hF }

Tactic:
congr

Goal state after:
case e_I
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I✝¹ : (n : ℕ) → Set (cell C n)
closed'✝¹ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
F : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] F
hF : D ∪ ⋃ n, ⋃ j, openCell n ↑j = F
h :
  (fun E ↦ E.carrier) { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    (fun E ↦ E.carrier) { carrier := F, I := I✝, closed' := closed'✝, union' := hF }
⊢ I✝¹ = I✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
x : I
⊢ c x = false

Tactic:
exact Bool.eq_false_iff.mpr (fun ht ↦ not_lt_zero (hsC c hc x ht))

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
⊢ D ∪ ((⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j) ∪ ⋃ j, closedCell n j) =
    D ∪ ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j

Tactic:
congr

Goal state after:
case e_a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
⊢ (⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j) ∪ ⋃ j, closedCell n j = ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j