mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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:
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.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ (tl_exp, tl_coef) ∈ Multiseries.cons tl_exp tl_coef tl_tl

Tactic:
simp [Multiseries.cons]

Goal state after:
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:
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.Defs

Goal state before:
pp: case h_coef.step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
⊢ ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → hd.2.Sorted ∧ motive tl

Tactic:
intro (exp, coef) tl h

Goal state after:
case h_coef.step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ (exp, coef).2.Sorted ∧ motive tl
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
⊢ ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → (∀ x ∈ tl.head, hd > x) ∧ motive tl

Tactic:
intro (exp, coef) tl h

Goal state after:
case step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ (∀ x ∈ tl.head, (exp, coef) > x) ∧ motive tl
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : g =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ g - basis_hd ^ exp * coef.toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun

Tactic:
h_eq

Goal state after:
case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : g =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ f - basis_hd ^ exp * coef.toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ (a % ↑n).toNat ∧ (a % ↑n).toNat < n ∧ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
by
    have := natCast_pos.2 <| Nat.le_of_ble_eq_true hn
    have nonneg := emod_nonneg a <| Int.ne_of_gt this
    refine ⟨Nat.zero_le _, ?_, ?_⟩
    · rw [Int.toNat_lt nonneg]; exact Int.emod_lt_of_pos _ this
    · rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]

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

Goal state before:
pp: a n : ℕ
h : IsNat a n
m k : ℕ
hm : m * m = k
hk₁ : k.blt n = true
hk₂ : n.ble (k + 2 * m) = true
⊢ ¬IsSquare a

Tactic:
by
  rcases h with ⟨rfl⟩
  subst k
  rintro ⟨b, rfl⟩
  simp only [Nat.blt_eq, Nat.ble_eq, ← sq, Nat.pow_lt_pow_iff_left two_ne_zero] at hk₁ hk₂
  rw [← Nat.add_one_le_iff, ← Nat.pow_le_pow_iff_left two_ne_zero] at hk₁
  grind

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

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSym (↑0) b = 0

Tactic:
Nat.cast_zero,

Goal state after:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSym 0 b = 0
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑a ^ b = ↑((a ^ b).mod n)

Tactic:
← Nat.cast_pow,

Goal state after:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b) = ↑((a ^ b).mod n)
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) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
K : Set X
hK : K ∈ 𝔖
⊢ UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
    UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)

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) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
K : Set X
hK : K ∈ 𝔖
this : CompactSpace ↑K
⊢ UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
    UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
have hxs : xs = TotalFunction.List.toFinmap' (xs₀.zip xs₁) := by
    rw [← h₀, ← h₁, List.toFinmap']; clear h₀ h₁ xs₀ xs₁ hperm hnodup
    induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ Injective (mapToSelf xs hperm hnodup).apply
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
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (K.domRestrict ∘ F) ℱ (𝓝 (K.domRestrict f))

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)

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
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (K.domRestrict ∘ F) ℱ (𝓝 (K.domRestrict f))
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
apply locallyCompactSpace_of_equicontinuousAt (U 0) (V 0) hU0c (hVo.mem_of_mem trivial)

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} := ⋯
U : ℕ → Set X := ⋯
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
⊢ EquicontinuousAt (fun f ↦ ⇑↑f) 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
this : 𝓕₁ = 𝓕₂
⊢ t₁ = t₂

Tactic:
rwa [IsTopologicalAddGroup.ext_iff] <;> infer_instance

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Valued R (WithZero (Multiplicative ℤ))
x : R
hx : v x ≤ exp (-1)
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0)

Tactic:
refine tendsto_zero_pow_of_v_lt_one (hx.trans_lt ?_)
  rw [← exp_zero, exp_lt_exp]
  simp

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

Goal state before:
pp: case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
a✝ : A.max' ⋯ + 1 ≤ m
⊢ IsEmpty (cell C m)

Tactic:
by_contra! h'

Goal state after:
case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
a✝ : A.max' ⋯ + 1 ≤ m
h' : Nonempty (cell C m)
⊢ False
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
S : Set X.A
⊢ IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
rw [← isOpen_compl_iff]
  constructor
  · intro cond F h
    by_contra c
    specialize cond F c
    rw [compl_mem_iff_notMem] at cond
    contradiction
  · intro h1 F h2
    specialize h1 F
    rcases F.mem_or_compl_mem S with h | h
    exacts [absurd (h1 h) h2, h]

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
J : Finset ι
⊢ ∀ (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})

Tactic:
s

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
J : Finset ι
s : ↑(obj C fun x ↦ x ∈ J)
⊢ IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
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
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC)))

Tactic:
refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩
      · refine eq_of_forall_π_app_eq a b (fun J ↦ ?_)
        apply_fun fun f : (limitCone.{u, u} (indexFunctor hC)).pt => f.val (op J) at h
        exact h
      · rsuffices ⟨b, hb⟩ : ∃ (x : C), ∀ (J : Finset ι), π_app C (· ∈ J) x = a.val (op J)
        · use b
          apply Subtype.ext
          apply funext
          intro J
          exact hb (unop J)
        have hc : ∀ (J : Finset ι) s, IsClosed ((π_app C (· ∈ J)) ⁻¹' {s}) := by
          intro J s
          refine IsClosed.preimage (π_app C (· ∈ J)).continuous ?_
          exact T1Space.t1 s
        have H₁ : ∀ (Q₁ Q₂ : Finset ι), Q₁ ≤ Q₂ →
            π_app C (· ∈ Q₁) ⁻¹' {a.val (op Q₁)} ⊇
            π_app C (· ∈ Q₂) ⁻¹' {a.val (op Q₂)} := by
          intro J K h x hx
          simp only [Set.mem_preimage] at hx ⊢
          rw [← map_comp_π_app C h, Function.comp_apply,
            hx, ← a.prop (homOfLE h).op]
          rfl
        obtain ⟨x, hx⟩ :
            Set.Nonempty (⋂ (J : Finset ι), π_app C (· ∈ J) ⁻¹' {a.val (op J)}) :=
          IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
            (fun J : Finset ι => π_app C (· ∈ J) ⁻¹' {a.val (op J)}) (directed_of_isDirected_le H₁)
            (fun J => (Set.singleton_nonempty _).preimage (surjective_π_app _))
            (fun J => (hc J (a.val (op J))).isCompact) fun J => hc J (a.val (op J))
        exact ⟨x, Set.mem_iInter.1 hx⟩

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ (1 - e (π C fun x ↦ x ∈ s) b) x = 1

Tactic:
· rw [LocallyConstant.sub_apply, e, LocallyConstant.coe_mk, LocallyConstant.coe_mk, if_neg hh]
    simp only [LocallyConstant.toFun_eq_coe, LocallyConstant.coe_one, Pi.one_apply, sub_zero]

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

Goal state before:
pp: case pos
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ord I i = o
⊢ true = g i

Tactic:
ord_term ho

Goal state after:
case pos
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : term I ho = i
⊢ true = g i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hi.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h2 : IsClosed[t] (A ∩ closedCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

Tactic:
exact h2

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
f : ↑(π (C1 C ho) fun x ↦ ord I x < o)
⊢ SwapTrue o ↑f ∈ C1 C ho

Tactic:
obtain ⟨f, g, hg, rfl⟩ := f
  convert! hg
  dsimp +unfoldPartialApp [SwapTrue]
  ext i
  split_ifs with h
  · rw [ord_term ho] at h
    simpa only [← h] using hg.2.symm
  · simp only [Proj, ite_eq_left_iff, not_lt, @eq_comm _ false, ← Bool.not_eq_true]
    specialize hsC g hg.1 i
    intro h'
    contrapose! hsC
    exact ⟨hsC, Order.succ_le_of_lt (h'.lt_of_ne' h)⟩

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

Goal state before:
pp: case inr
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
x : I → Bool
i : I
hi✝ : o ≤ ord I i
hi : ord I i = o
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i

Tactic:
ord_term ho

Goal state after:
case inr
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
x : I → Bool
i : I
hi✝ : o ≤ ord I i
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ord I i = o
⊢ true = x i

Tactic:
ord_term ho

Goal state after:
case pos
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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : term I ho = i
⊢ true = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case inl
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
h✝ : C = ∅
⊢ LinearIndependent ℤ (eval C)

Tactic:
subst C

Goal state after:
case inl
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
x✝ : IsClosed ∅
hsC : contained ∅ 0
⊢ LinearIndependent ℤ (eval ∅)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case inr
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
h✝ : C = {fun x ↦ false}
⊢ LinearIndependent ℤ (eval C)

Tactic:
subst C

Goal state after:
case inr
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
x✝ : IsClosed {fun x ↦ false}
hsC : contained {fun x ↦ false} 0
⊢ LinearIndependent ℤ (eval {fun x ↦ false})
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case pos
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
j : cell C n
h : j ∈ I n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
right
      suffices closedCell n j ⊆ E by
        rw [inter_eq_right.2 this]
        exact isClosed_closedCell
      exact closedCell_subset n ⟨j, h⟩

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✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ C

Tactic:
← RelCWComplex.union_iUnion_openCell_eq_complex

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ D ∪ ⋃ n, ⋃ j, openCell n j