mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ j ∈ univ

Tactic:
by simp

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (μIso (free R) P S.toCondensed).hom ≫ g = g' ≫ e
⊢ (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g = ((μIso (free R) P S'.toCondensed).inv ≫ g') ≫ e

Tactic:
rw [assoc, ← hh]

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (μIso (free R) P S.toCondensed).hom ≫ g = g' ≫ e
⊢ (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g =
    (μIso (free R) P S'.toCondensed).inv ≫
      (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (μIso (free R) P S.toCondensed).hom ≫ g
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj S'.toCondensed ⊗ (free R).obj P ⟶ A
hh : (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ (μIso (free R) S.toCondensed P).hom ≫ g = g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g = ((μIso (free R) S'.toCondensed P).inv ≫ g') ≫ e

Tactic:
rw [assoc, ← hh]

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj S'.toCondensed ⊗ (free R).obj P ⟶ A
hh : (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ (μIso (free R) S.toCondensed P).hom ≫ g = g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g =
    (μIso (free R) S'.toCondensed P).inv ≫
      (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ (μIso (free R) S.toCondensed P).hom ≫ g
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X : CondensedSet
⊢ IsIso compactlyGeneratedAdjunction.counit

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
X : CondensedSet
⊢ ∀ (X : CompactlyGenerated), IsIso (compactlyGeneratedAdjunction.counit.app X)
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P.toCondensed ⊗ S'.toCondensed) ⟶ A
hh :
  (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet P S').inv ≫ g') ≫ e

Tactic:
rw [assoc, ← hh]

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P.toCondensed ⊗ S'.toCondensed) ⟶ A
hh :
  (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet P S').inv ≫
      (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫
        (free R).map (μIso lightProfiniteToLightCondSet P S).hom ≫ g
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S').toCondensed ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).inv ≫ g =
    g' ≫ e
⊢ (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet P S').hom ≫ g') ≫ e

Tactic:
rw [assoc, ← hh]

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S').toCondensed ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).inv ≫ g =
    g' ≫ e
⊢ (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet P S').hom ≫
      (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫
        (free R).map (μIso lightProfiniteToLightCondSet P S).inv ≫ g
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S ⊗ P).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P.toCondensed) ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet S' P).inv ≫ g') ≫ e

Tactic:
rw [assoc, ← hh]

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S ⊗ P).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P.toCondensed) ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet S' P).inv ≫
      (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
        (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S' ⊗ P).toCondensed ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet S' P).hom ≫ g') ≫ e

Tactic:
rw [assoc, ← hh]

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S' ⊗ P).toCondensed ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet S' P).hom ≫
      (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
        (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = Fix.approx f (Nat.succ 0) x'

Tactic:
Fix.approx,

Goal state after:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = f (Fix.approx f 0) x'
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = Fix.approx f (n + 1).succ x'

Tactic:
Fix.approx,

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = f (Fix.approx f (n + 1)) x'
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun b a ↦ b ∈ f a) [] []

Tactic:
by simp

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun b a ↦ b ∈ f a) [] (a :: as)

Tactic:
by simp

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun b a ↦ b ∈ f a) (b :: bs) []

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∉ Finset.map { toFun := fs, inj' := ⋯ } elems

Tactic:
by simp

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse =
    (List.foldr cons [] (FreeMonoid.toList (foldMap FreeMonoid.of xs)).reverse).reverse

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ f = f' ∧ g = g'

Tactic:
← dropFun_splitFun f g,

Goal state after:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f g) = f' ∧ g = g'
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : TypeVec.{?u.30} (n + 1) → Sort u_1
f : (t : Type ?u.30) → (v : TypeVec.{?u.30} n) → β (v ::: t)
v : TypeVec.{?u.30} (n + 1)
⊢ β (v.drop ::: v.last) = β v

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (OnePoint.some ⁻¹' {↑i})

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ σ (Option.some x) s ∈ fibres π σ

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ subtypeVal p ⊚ toSubtype p = fun x ↦ Subtype.val

Tactic:
by
  ext i x
  induction i <;> simp only [toSubtype, comp, subtypeVal] at *
  simp [*]

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
rw [traverse_def, comp_traverse, Comp.map_mk]

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk ((fun x ↦ ⇑(eqv γ) <$> x) <$> traverse f <$> traverse g ((eqv α).symm x)) =
    Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
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 simp

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 simp

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 simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f < toMultiset g ↔ f < g

Tactic:
simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊓ g)) = Multiset.toDFinsupp (toMultiset f ∩ toMultiset g)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊔ g)) = Multiset.toDFinsupp (toMultiset f ∪ toMultiset g)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
q : Semiquot α
⊢ ∀ (a : α), a ∈ id <$> q ↔ a ∈ q

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β : Type u_3
x : α
f : α → Semiquot β
⊢ ∀ (a : β), a ∈ pure x >>= f ↔ a ∈ f x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ xs.get ((fun x ↦ ⟨List.idxOf x xs, ⋯⟩) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : PUnit.{?u.8 + 1}
⊢ x ∈ [PUnit.unit]

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ ∀ (x : Fin n), x ∈ List.finRange n

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n✝ : ℕ
α : Type u_2
m : ℕ
h : m ≤ n✝
v : Fin n✝ → α
n : ℕ
h1 : n < (List.ofFn (take m h v)).length
h2 : n < (List.take m (List.ofFn v)).length
⊢ (List.ofFn (take m h v)).get ⟨n, h1⟩ = (List.take m (List.ofFn v)).get ⟨n, h2⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
n : ℕ
h1 : n < (List.ofFn (take m h l.get)).length
h2 : n < (List.take m l).length
⊢ (List.ofFn (take m h l.get)).get ⟨n, h1⟩ = (List.take m l).get ⟨n, h2⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))

Tactic:
simp only [or_iff_not_imp_left] at hs

Goal state after:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, ¬x_1 = x → x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : Finset α), x ∈ enum (toList α)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Type v
inst✝¹ : (a : α) → FinEnum (β a)
inst✝ : Decidable α
h : α
x✝ : (a : α) ×' β a
a : α
Ba : β a
⊢ ⟨a, Ba⟩ ∈ List.map (PSigma.mk h) (toList (β h))

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ (a : α), β a
⊢ ∀ (x : (a : α) ×' β a), x ∈ [⟨⋯, ⋯⟩]

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
⊢ ∀ (x : { x // x ∈ xs }), x ∈ xs.attach

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ e = { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
change FinEnum.mk e.1 e.2 = _

Goal state after:
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ { card := card α, equiv := equiv, decEq := fun a b ↦ decEq a b } =
    { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun a b ↦ decidableEq_of_subsingleton a b }
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ e = { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
change FinEnum.mk e.1 e.2 = _

Goal state after:
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ { card := card α, equiv := equiv, decEq := fun a b ↦ decEq a b } =
    { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun a b ↦ decidableEq_of_subsingleton a b }
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case trans
α : Type u_1
f : α → Option α
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝ → lookmap f l₁✝ ~ lookmap f l₂✝
IH₂ : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂✝ → lookmap f l₂✝ ~ lookmap f l₃✝
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
⊢ lookmap f l₁✝ ~ lookmap f l₃✝

Tactic:
| trans p₁ _ IH₁ IH₂ =>

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : AList β
⊢ (s ∪ ∅).entries = s.entries

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
⊢ dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)

Tactic:
induction l₁ with

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ lookupAll a [] = [] ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ []

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ (lookupAll a []).head? = dlookup a []

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ b ∈ lookupAll a [] ↔ ⟨a, b⟩ ∈ []

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ map (Sigma.mk a) (lookupAll a []) <+ []

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : Finmap β
⊢ ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ })
        ((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩) f)).entries =
    f.entries

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: ⊢ ∀ {α : Type u_1} (x : Multiset α), id <$> x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: ⊢ ∀ {α β γ : Type u_1} (g : α → β) (h : β → γ) (x : Multiset α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ (replace a b ⟦s⟧).keys = ⟦s⟧.keys

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
s : AList β
⊢ a' ∈ replace a b ⟦s⟧ ↔ a' ∈ ⟦s⟧

Tactic:
by simp

Goal state after: