mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.ofEquiv E F.F).toFilter.sets
s : τ
h : (CFilter.ofEquiv E F.F).f s ⊆ x✝¹
⊢ F.F.f (E.symm s) ⊆ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ F.F.toFilter.sets
t : F.σ
h : F.F.f t ⊆ x✝¹
⊢ (CFilter.ofEquiv E F.F).f (E t) ⊆ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
⊢ (CFilter.ofEquiv E F.F).toFilter = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.AllAny

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (l.all fun a ↦ decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ f (E.symm (E (T x)))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.AllAny

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (l.any fun a ↦ decide (p a)) = true ↔ ∃ a, a ∈ l ∧ p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ x✝ ∈ { f := fun s ↦ m '' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (map m f).sets

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ x ∈ f (E.symm (E (I (E.symm a) (E.symm b) x h)))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ f (E.symm (E (I (E.symm a) (E.symm b) x h))) ⊆ f (E.symm a) ∩ f (E.symm b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
F : f.Realizer
x✝ : Set α
⊢ x✝ ∈ { f := fun s ↦ m ⁻¹' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m f).sets

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ 𝟙 T ≫ π = 𝟙 T ≫ π

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ (CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
      π =
    (CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
      π

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
F : Ctop α σ
a : τ
⊢ (ofEquiv E F).f a = F.f (E.symm a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ (CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
      π =
    (CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
      π

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : f.Realizer
G : g.Realizer
x✝ : Set α
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => F.F.f s ∪ G.F.f t,
            pt := (F.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (F.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ F.F.f s
⊢ 𝓝 a ≤ 𝓟 (F.F.f s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
⊢ F.toTopsp = T

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s✝ : Set α
x✝ : ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s✝
s : F.σ
h : a ∈ F.F.f s ∧ F.F.f s ⊆ s✝
⊢ a ∈ (Ctop.ofEquiv E F.F).f (E s) ∧ (Ctop.ofEquiv E F.F).f (E s) ⊆ s✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s : Set α
x✝ : ∃ b, a ∈ (Ctop.ofEquiv E F.F).f b ∧ (Ctop.ofEquiv E F.F).f b ⊆ s
t : τ
h : a ∈ (Ctop.ofEquiv E F.F).f t ∧ (Ctop.ofEquiv E F.F).f t ⊆ s
⊢ a ∈ F.F.f (E.symm t) ∧ F.F.f (E.symm t) ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ (F.ofEquiv E).F.f s = F.F.f (E.symm s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ { a // a ∈ ∅ ∧ 𝓝 a ⊓ f ≠ ⊥ }

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case right
R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
this :
  cover π =
    ↑(BinaryCofan.IsColimit.desc'
        (coproductIsColimit T
          (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
            (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))
        (CompHausLike.pullback.lift π π (𝟙 T) (𝟙 T) ⋯)
        (CompHausLike.pullback.lift π π
          (CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
              (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
          (CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
              (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
          ⋯))
⊢ (free R).map
        (lightProfiniteToLightCondSet.map
          (((((CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                      (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                  π) ≫
                fst S ℕ∪{∞}) ≫
              σ) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
      g =
    (free R).map
        (lightProfiniteToLightCondSet.map
          (((((CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                      (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                  π) ≫
                fst S ℕ∪{∞}) ≫
              σ) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
      g

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ Cocone
    (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
        (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
      free R)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : f.Realizer
G : g.Realizer
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => F.F.f s ∩ G.F.f t,
        pt := (F.F.pt, G.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (F.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
⊢ Continuous ⇑(ConcreteCategory.hom π)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : DecidableEq α
x✝ : Set α
h : x✝ ∈ cofinite.sets
⊢ { f := fun s ↦ {a | a ∉ s}, pt := ∅, inf := fun x1 x2 ↦ x1 ∪ x2, inf_le_left := ⋯, inf_le_right := ⋯ }.f
      (Finite.toFinset h) ⊆
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
n : ↑ℕ∪{∞}.toTop
⊢ Continuous fun x ↦ ↑x n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f✝ : Filter α
m : α → Filter β
F : f✝.Realizer
G : (i : α) → (m i).Realizer
x✝ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
s : F.σ
f : (i : α) → i ∈ F.F.f s → (G i).σ
i : α
h✝ : i ∈ F.F.f s
⊢ i ∈ F.F.f s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x✝ : β
⊢ (x✝ ∈
      match
        match x✝² with
        | ⟨a, f_1⟩ =>
          match x✝¹ with
          | ⟨b, f'⟩ => ⟨F.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩ with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)) →
    x✝ ∈
      match x✝² with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x✝ : β
⊢ (x✝ ∈
      match
        match x✝² with
        | ⟨a, f_1⟩ =>
          match x✝¹ with
          | ⟨b, f'⟩ => ⟨F.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩ with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)) →
    x✝ ∈
      match x✝¹ with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.FiniteInfinite

Goal state before:
pp: ι✝ : Type u
γ : Type w
β : ι✝ → Type v
β₁ : ι✝ → Type v₁
β₂ : ι✝ → Type v₂
ι : Type u_1
π : ι → Type u_2
inst✝² : ∀ (i : ι), Nontrivial (π i)
inst✝¹ : (i : ι) → Zero (π i)
inst✝ : Infinite ι
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
⊢ (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π =
    lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
        (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
      y' ▷ ℕ∪{∞}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝ : Set β
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h),
            pt := ⟨F.F.pt, fun i x ↦ (G i).F.pt⟩,
            inf := fun x x_1 ↦
              match x with
              | ⟨a, f_1⟩ =>
                match x_1 with
                | ⟨b, f'⟩ => ⟨F.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩,
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f.bind m).sets

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : α → Filter β
F : (i : α) → (f i).Realizer
⊢ ∀ (x : Set β), x ∈ (⊤.bind f).sets ↔ x ∈ (⨆ i, f i).sets

Tactic:
by

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
⊢ Continuous ⇑(ConcreteCategory.hom π')

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
⊢ ∀ (x : Option ℕ), Continuous (σ' x)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Continuous Subtype.val

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ Function.Injective fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (∃ a ∈ s.pi t, { toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } a = f) →
    f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
rintro ⟨f, hf, rfl⟩
    rw [Function.Embedding.coeFn_mk]
    refine ⟨support_mk_subset, fun i hi => ?_⟩
    convert! mem_pi.1 hf i hi
    exact mk_of_mem hi

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
b : Bool
⊢ count (!b) l + count b l = l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
b : Bool
⊢ count b l + count (!b) l = l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: b x : Bool
l : List Bool
h : IsChain (fun x1 x2 ↦ x1 ≠ x2) (b :: x :: l)
⊢ count (!b) (x :: l) = count b (x :: l) + (x :: l).length % 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ count (!b) l = count b l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ count (!b) l ≤ count b l + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
⊢ f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ 2 * count b l = l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
⊢ Icc (f i) (g i) = 0

Tactic:
by

Goal state after: