mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Type (u + 1)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) (lanPresheaf (locallyConstantPresheaf X))

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso
      fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]

Goal state after:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Type (u + 1)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) (locallyConstantPresheaf X)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
⊢ ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app S =
    ((lanPresheafNatIso fun x ↦
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).hom ≫
          counitApp X).app
      S

Tactic:
apply colimit.hom_ext

Goal state after:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
          S =
      colimit.ι
          (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafNatIso fun x ↦
                  isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).hom ≫
              counitApp X).app
          S
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F)
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
        (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
        (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) =
    colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.hom)

Tactic:
apply colimit.hom_ext

Goal state after:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
            (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j ≫
        colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.hom)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
        (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
        (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) =
    colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.inv)

Tactic:
apply colimit.hom_ext

Goal state after:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
            (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.inv)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (lanPresheaf (locallyConstantPresheaf X))

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso
      fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]

Goal state after:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (locallyConstantPresheaf X)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app S =
    ((lanPresheafNatIso fun x ↦
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).hom ≫
          counitApp X).app
      S

Tactic:
apply colimit.hom_ext

Goal state after:
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
          S =
      colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafNatIso fun x ↦
                  isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
                    x).hom ≫
              counitApp X).app
          S
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
⊢ x ∈ C i ∩ C j

Tactic:
by grind

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀) a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
replace h₁ := approx_mono' f _ _ h₁

Goal state after:
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.fst Fin2.fz (prod.mk Fin2.fz a b) = a

Tactic:
simp_all only [prod.fst, prod.mk]

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
y : T
hy : π y = (s, none)
⊢ y ∈ fibres π σ

Tactic:
by grind

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
⊢ ((fun x ↦ π ↑x) ⟨σ (Option.some x) s, ⋯⟩).1 = (s, Option.some x).1

Tactic:
by grind

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
⊢ ((fun x ↦ π ↑x) ⟨σ (Option.some x) s, ⋯⟩).2 = (s, Option.some x).2

Tactic:
by grind

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
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ ⟨t, ht⟩ ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
by grind

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
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ ⟨t', ht'⟩ ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
by grind

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
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ π_r π σ (fibreIncl π σ (⟨⟨t, ht⟩, ⋯⟩, ⟨⟨t', ht'⟩, ⋯⟩).1) = π_r π σ (fibreIncl π σ (⟨⟨t, ht⟩, ⋯⟩, ⟨⟨t', ht'⟩, ⋯⟩).2)

Tactic:
by grind

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
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ coverToFun (fibreIncl π σ) (π_r π σ) (Sum.inr ⟨(⟨⟨t, ht⟩, ⋯⟩, ⟨⟨t', ht'⟩, ⋯⟩), ⋯⟩) = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
by grind

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
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ σ (Option.some n) (π t).1 ∈ fibres π σ

Tactic:
by grind

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
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ coverToFun (fibreIncl π σ) (π_r π σ) (Sum.inl ⟨σ (Option.some n) (π t).1, ⋯⟩) = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
by grind

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ σ none s ∈ fibres π σ

Tactic:
by grind

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ ⟨σ none s, ⋯⟩ ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
by grind

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 × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
n : OnePoint X
⊢ p s n ∈ Prod.snd ∘ π ⁻¹' {n}

Tactic:
by grind

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 × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ (fun n ↦ ⟨p s n, ⋯⟩) ∈ S' π

Tactic:
by grind

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 × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ y π ⟨fun n ↦ ⟨p s n, ⋯⟩, ⋯⟩ = s

Tactic:
by grind

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✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ IsCompact (⋂ n, ⋂ m, {x | (π ↑(x n)).1 = (π ↑(x m)).1})

Tactic:
have (x : OnePoint X) : CompactSpace <| (Prod.snd ∘ π) ⁻¹' {x} :=
    isCompact_iff_compactSpace.mp (IsClosed.preimage (by fun_prop) isClosed_singleton).isCompact

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace ↑(Prod.snd ∘ π ⁻¹' {x})
⊢ IsCompact (⋂ n, ⋂ m, {x | (π ↑(x n)).1 = (π ↑(x m)).1})
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:
by
    change FinEnum.mk e.1 e.2 = _
    congr 1
    · exact card_eq_zero
    · refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
      exact congrArg (α ≃ Fin ·) <| card_eq_zero
    · funext x
      exact ‹IsEmpty α›.elim x

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

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
⊢ s₁.keys ⊆ s₂.keys

Tactic:
intro k hk

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
⊢ k ∈ s₂.keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
h : (s :: l).NodupKeys
⊢ ¬s.fst ∈ l.keys

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
a : α
b : β a
⊢ b ∈ lookup a s ↔ ⟨a, b⟩ ∈ s.entries

Tactic:
rcases s with ⟨⟨l⟩, hl⟩

Goal state after:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l)
⊢ b ∈ lookup a { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl } ↔
    ⟨a, b⟩ ∈ { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl }.entries
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
h1 : (lookupAll a l).length ≤ 1
⊢ lookupAll a l = (lookupAll a l).head?.toList

Tactic:
revert h1

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1 → lookupAll a l = (lookupAll a l).head?.toList
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by
  convert! hs.toFinset.exists_between' ht.toFinset (by simpa) using 1; simp

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

Goal state before:
pp: case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a✝ : List α
⊢ (fun a ↦ h <$> ↑a) <$> Traversable.traverse g a✝ =
    ofList <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝

Tactic:
simp only [fmap_def, Function.comp_apply, Functor.map_map, List.map_eq_map, map_coe]

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

Goal state before:
pp: case refine_2
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s ↦ decide (a = s.fst)) a_1 → a_1 = b

Tactic:
· simp

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
this : IsIso π'
⊢ (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f =
    ((lightProfiniteToLightCondSet ⋙ free R).map (CategoryTheory.inv π' ≫ g') ≫ g) ≫ p

Tactic:
by grind

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

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ (∃ i ∈ image (const β✝) s, a ∈ image i t) → a ∈ s

Tactic:
rintro ⟨f, hf, ha⟩

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
f : β✝ → α✝
hf : f ∈ image (const β✝) s
ha : a ∈ image f t
⊢ a ∈ s
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ (∃ i ∈ image (const α✝ id) s, a ∈ image i t) → a ∈ t

Tactic:
rintro ⟨f, hf, ha⟩

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
f : β✝ → β✝
hf : f ∈ image (const α✝ id) s
ha : a ∈ image f t
⊢ a ∈ t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

Tactic:
by_cases h : a = a'
  · subst a'; rfl
  induction l with
  | nil => rfl
  | cons x xs =>
    by_cases a' = x.1
    · subst a'
      simp [kerase_cons_ne h, kerase_cons_eq rfl]
    by_cases h' : a = x.1
    · subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
    · simp [kerase_cons_ne, *]

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

Goal state before:
pp: case cons.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
tail✝ : List (Sigma β)
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
ih :
  ∀ {l₂ : List (Sigma β)},
    ⟨a', snd✝⟩.fst ∈ tail✝.keys → dlookup ⟨a', snd✝⟩.fst (tail✝.kunion l₂) = dlookup ⟨a', snd✝⟩.fst tail✝
⊢ dlookup ⟨a', snd✝⟩.fst ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup ⟨a', snd✝⟩.fst (⟨a', snd✝⟩ :: tail✝)

pp: case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
· simp

Goal state after:
case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case hp
m n i j : ℕ
⊢ (↑i).bodd = ((j + i).bodd ^^ j.bodd)

Tactic:
simp only [Int.bodd, Nat.bodd_add]

Goal state after:
case hp
m n i j : ℕ
⊢ i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case hn
m n i j : ℕ
⊢ -[i+1].bodd = (j.bodd ^^ (j + i + 1).bodd)

Tactic:
simp only [Int.bodd, Nat.bodd_add]

Goal state after:
case hn
m n i j : ℕ
⊢ (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

pp: case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
· simp

Goal state after:
case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || y)) m n = Nat.bitwise (fun a b ↦ a && !b) m n

pp: case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n

Tactic:
· simp

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℕ
h : (↑a ≤ ↑x ∧ ↑x < ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ((a ≤ x ∧ x < b) ∧ x ≡ v [MOD r]) ∧ ↑x = ↑x

Tactic:
by simp_all [natCast_modEq_iff]

Goal state after: