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

Goal state before:
pp: case eq.inr.inr.lt
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : Ordering.lt.Compares a₁ a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
dsimp at IHa

Goal state after:
case eq.inr.inr.lt
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ < a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : Ordering.eq.Compares a₁ a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
dsimp at IHa

Goal state after:
case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ = a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inr.inr.gt
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : Ordering.gt.Compares a₁ a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
dsimp at IHa

Goal state after:
case eq.inr.inr.gt
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ > a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c✝ : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
let ⟨d, hd⟩ := γδ (by rwa [ea] at c)

Goal state after:
case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c✝ : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
d : δ
hd : (Γ (⋯.mp c)).Equiv (Δ d)
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
e : z = f y
⊢ ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z

Tactic:
by
        subst e
        exact ⟨_, h, rfl⟩

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

Goal state before:
pp: case pos
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : some x :: ↑s = some x :: ↑t
⊢ False

Tactic:
contrapose! h'

Goal state after:
case pos
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h_if : some x :: ↑s = some x :: ↑t
h' : True
⊢ Seq.cons x s = Seq.cons x t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: 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'))

Tactic:
change f b' = T f b'

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' = T f b'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
⊢ (a.oadd m b).FundamentalSequenceProp (a.oadd m b).fundamentalSequence

Tactic:
rw [fundamentalSequence]

Goal state after:
case oadd
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
⊢ (a.oadd m b).FundamentalSequenceProp
    (match b.fundamentalSequence with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: b : ℕ
⊢ jacobiSym 1 b = 1

Tactic:
jacobiSym.one_left

Goal state after:
b : ℕ
⊢ 1 = 1
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
⊢ (b :: l).prod = n

Tactic:
by rw [List.prod_cons, f₃, h₁.out, cast_id]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
H' : Tendsto (⇑UniformFun.ofFun ∘ Subtype.val) 𝒢 (𝓝 ((⇑UniformFun.ofFun ∘ Subtype.val) ⟨f, f_mem⟩))
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
← tendsto_map'_iff,

Goal state after:
case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
H' : Tendsto (⇑UniformFun.ofFun) (map Subtype.val 𝒢) (𝓝 ((⇑UniformFun.ofFun ∘ Subtype.val) ⟨f, f_mem⟩))
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun 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
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
have hU4 : ∀ f : X →* Y, Set.MapsTo f (U 0) (V 0) → ∀ n, Set.MapsTo f (U n) (V n) := by
    intro f hf n
    induction n with
    | zero => exact hf
    | succ n ih =>
      exact fun x hx ↦ hV (ih (hU3 n hx)) (map_mul f x x ▸ ih (hU2 n (Set.mul_mem_mul hx hx)))

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} :=
  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)
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
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun x_1 ↦ x ^ x_1

Tactic:
rw [← mapClusterPt_atTop_zpow_iff_pow]

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun x_1 ↦ x ^ x_1
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f f' : M → E
g : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
⊢ (f + f') ⋆[L] g = f ⋆[L] g + f' ⋆[L] g

Tactic:
by
  ext x; exact (hfg x).add_distrib L (hfg' x)

Goal state after:
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
V_mem : V ∈ 𝓝 0
H : TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂
⊢ t₁ = t₂

Tactic:
apply topology_eq_of_nhds_inf_principal_eq 𝕜₁ t₁ t₂ V_mem
  set o : V := ⟨0, letI := t₁; mem_of_mem_nhds V_mem⟩
  simp_rw [← map_comap_setCoe_val, show 0 = (o : E) from rfl, ← nhds_induced]
  rw [H]

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
h : α ≃ₜ β
⊢ map (⇑h) (residual α) = residual β

Tactic:
refine le_antisymm (tendsto_residual_of_isOpenMap h.continuous h.isOpenMap) (le_map ?_)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, ⇑h '' s ∈ residual β
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: 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
S1 : Set X.A
hS1 : S1 ∈ F
S2 : Set X.A
hS2 : S2 ∈ F
⊢ basic S1 ∩ basic S2 = basic (S1 ∩ S2)

Tactic:
simp [basic_inter]

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

Goal state before:
pp: 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
⊢ X.str F = x

Tactic:
have claim3 : ∀ (S1) (_ : S1 ∈ T0) (S2) (_ : S2 ∈ T0), S1 ∩ S2 ∈ T0 := by
    rintro S1 ⟨S1, hS1, rfl⟩ S2 ⟨S2, hS2, rfl⟩
    exact ⟨S1 ∩ S2, inter_mem hS1 hS2, by simp [basic_inter]⟩

Goal state after:
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
⊢ X.str F = x
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 : ι → Prop
x : ↑(obj C J)
y : (i : ι) → X i
hy : y ∈ C ∧ (precomp Subtype.val) y = ↑x
⊢ ∃ a, (π_app C J) a = x

Tactic:
exact ⟨⟨y, hy.1⟩, Subtype.ext hy.2⟩

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

Goal state before:
pp: I : Type u_1
C : Set (I → Bool)
x : ↑C
l : List (LocallyConstant ↑C ℤ)
⊢ l.prod x = (List.map (⇑(LocallyConstant.evalMonoidHom x)) l).prod

Tactic:
by
  rw [← map_list_prod (LocallyConstant.evalMonoidHom x) l, LocallyConstant.evalMonoidHom_apply]

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
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
h' : openCell n i = ∅
⊢ False

Tactic:
exact notMem_empty _ (h' ▸ map_zero_mem_openCell n i)

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
⊢ IsClosed[t] C

Tactic:
closed C C (by rfl)

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ (∀ (n : ℕ) (j : cell C n), IsClosed[t] (C ∩ closedCell n j)) ∧ IsClosed[t] (C ∩ D)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
⊢ e (π C fun x ↦ x ∈ s) a * Products.eval (π C fun x ↦ x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
apply Submodule.subset_span

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
⊢ e (π C fun x ↦ x ∈ s) a * Products.eval (π C fun x ↦ x ∈ s) m ∈
    Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as}
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case nil
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a✝ : List.IsChain (fun x1 x2 ↦ x1 > x2) []
⊢ (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) []).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ []})

Tactic:
apply Submodule.subset_span

Goal state after:
case nil
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a✝ : List.IsChain (fun x1 x2 ↦ x1 > x2) []
⊢ (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) []).prod ∈
    Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ []}
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg.h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
⊢ Products.eval (π C fun x ↦ x ∈ s) m ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
apply Submodule.subset_span

Goal state after:
case neg.h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
⊢ Products.eval (π C fun x ↦ x ∈ s) m ∈ Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as}
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}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h : Continuous fun f ↦ f (term I ho)
⊢ IsClosed {f | f (term I ho) = false}

Tactic:
exact IsClosed.preimage h (t := {false}) (isClosed_discrete _)

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

Goal state before:
pp: case neg
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
h : ¬ord I i < o
⊢ false = x i

Tactic:
simp only [not_lt] at h

Goal state after:
case neg
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
h : o ≤ ord I i
⊢ false = x i
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₂
g : LocallyConstant ↑(π C fun x ↦ ord I x < o₁) ℤ
hg : g ∈ range (π C fun x ↦ ord I x < o₁)
⊢ (πs' C h) g ∈ range (π C fun x ↦ ord I x < o₂) ∧ (πs C o₂) ((πs' C h) g) = (πs C o₁) g

Tactic:
obtain ⟨⟨l, gl⟩, rfl⟩ := hg

Goal state after:
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⟩)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
x : ↑C
⊢ (∀ i ∈ ↑l, ↑x i = true) → False

Tactic:
contrapose! h'

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
x : ↑C
h' : (∀ i ∈ ↑l, ↑x i = true) ∧ True
⊢ ord I i < o
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent (ι := ↑(GoodProducts (π C fun x ↦ ord I x < o))) ℤ (eval (π C fun x ↦ ord I x < o))

pp: case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent (ι := ↑(MaxProducts C ho')) ℤ
    (⇑(CategoryTheory.ConcreteCategory.hom
          { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
              X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho') ℤ),
              f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho'), zero := ⋯ }.g) ∘
      SumEval C ho' ∘ Sum.inr)

Tactic:
· exact h (le_of_lt ho') (π C (ord I · < o)) (isClosed_proj C o hC) (contained_proj C o)

Goal state after:
case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent (ι := ↑(MaxProducts C ho')) ℤ
    (⇑(CategoryTheory.ConcreteCategory.hom
          { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
              X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho') ℤ),
              f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho'), zero := ⋯ }.g) ∘
      SumEval C ho' ∘ Sum.inr)