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

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
⊢ (ConcreteCategory.hom ((ObjectProperty.homMk (counitApp ((functor P hs).obj X).obj)).hom.app (op S)))
      (map (fun x ↦ LocallyConstant.const PUnit.{u + 1} x) f) =
    f

Tactic:
apply presheaf_ext
    (X := ((functor P hs).obj X).obj) (Y := ((functor.{u, w} P hs).obj X).obj)
      (f.map ((unit P hs).app X))

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
⊢ ∀ (a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)),
    (ConcreteCategory.hom
          (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
        ((ConcreteCategory.hom ((ObjectProperty.homMk (counitApp ((functor P hs).obj X).obj)).hom.app (op S)))
          (map (fun x ↦ LocallyConstant.const PUnit.{u + 1} x) f)) =
      (ConcreteCategory.hom
          (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
        f
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functorIsoDiscreteAux₂ R X✝).hom ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
← Iso.eq_inv_comp,

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
inst✝¹ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A
F : Profiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functorIsoDiscreteAux₂ R X✝).hom ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
← Iso.eq_inv_comp,

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : Profiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
F : CompHausᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : CompHausᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩

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

Goal state before:
pp: X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → ↑X.toLightCondSet.toTopCat :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ ⇑(OnePoint.continuousMapMkNat f p h)
⊢ Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
    (nhds ((topCatAdjunctionCounitEquiv X).invFun p))

Tactic:
change Filter.Tendsto (fun n : ℕ ↦ g n) _ _

Goal state after:
X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → ↑X.toLightCondSet.toTopCat :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ ⇑(OnePoint.continuousMapMkNat f p h)
⊢ Filter.Tendsto (fun n ↦ g ↑n) Filter.atTop (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
Module: Mathlib.Condensed.Light.Explicit

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
F : LightProfiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : LightProfiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (counitAppApp (LightProfinite.of (Opposite.unop Y).obj) X)) f)

Tactic:
rw [incl_of_counitAppApp]

Goal state after:
case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    counitAppAppImage f x
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)

Tactic:
rw [← comp_traverse]

Goal state after:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α : Type u_1
xs : List α
⊢ List.traverse pure xs = pure xs

Tactic:
induction xs

Goal state after:
case nil
α : Type u_1
⊢ List.traverse pure [] = pure []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = pure tail✝
⊢ List.traverse pure (head✝ :: tail✝) = pure (head✝ :: tail✝)
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = (ConcreteCategory.hom (unop ((Foldl.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))))) x

Tactic:
simp only [foldl, toList_spec, foldMap_hom_free, foldl.ofFreeMonoid_comp_of, Foldl.get,
    FreeMonoid.ofList_toList]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ ((fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y) =
    ((fun i x ↦ (↑(f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x ↦ (↑(f' rr n α i x)).2) <$$> u✝ = y)

Tactic:
congr <;> ext i ⟨x, _⟩ <;> cases i

Goal state after:
case h₁.e_a.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).1

case h₁.e_a.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).1

case h₁.e_b.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).2

case h₁.e_b.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).2
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:
delta ofEquiv

Goal state after:
α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ }.F.f s = F.F.f (E.symm s)
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ x ∈ (f.support ∪ g.support).dfinsupp ⇑(f.rangeIcc g) ↔ f ≤ x ∧ x ≤ g

Tactic:
by
      refine (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans ?_
      simp_rw [mem_rangeIcc_apply_iff, forall_and]
      rfl

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case h₁
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i ≤ f a k

pp: case h
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a✝¹ : α
s : Finset α
ha : a✝¹ ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
a✝ : a ∈ s
⊢ f a j ≤ f a k

Tactic:
exacts [(hk a).1, (hk _).2]

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m : ℕ
v : ValidFinite e m
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ ValidFinite e m'

Tactic:
by unfold ValidFinite at *; rw [ss]; exact v

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

Goal state before:
pp: α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih : tl.NodupKeys → (map (Sigma.map f fun x ↦ id) tl).NodupKeys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
h : (Sigma.map f (fun x ↦ id) hd).fst ∈ map (Sigma.fst ∘ Sigma.map f fun x ↦ id) tl
x : (_ : α) × β
hm : x ∈ tl
he : (Sigma.fst ∘ Sigma.map f fun x ↦ id) x = (Sigma.map f (fun x ↦ id) hd).fst
⊢ hd.fst ∈ map Sigma.fst tl

Tactic:
exact mem_map.mpr ⟨x, hm, hf he⟩

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
⊢ IsEmpty ↑S'.toTop

Tactic:
simpa using hS'

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 : α → β
h : β → G γ
a✝ : List α
⊢ ofList <$> Traversable.traverse h (List.map g a✝) = ofList <$> Traversable.traverse (h ∘ g) a✝

Tactic:
rw [← Traversable.traverse_map h g, List.map_eq_map]

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 β✝
hs : s.Nonempty
a : β✝
⊢ (a ∈ if s = ∅ then ∅ else t) ↔ a ∈ (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
if_neg hs.ne_empty,

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys
l₂ : List (Sigma β)
h : ¬a = s.fst
⊢ a ∈ ((s :: l₁).kunion l₂).keys ↔ a ∈ (s :: l₁).keys ∨ a ∈ l₂.keys

Tactic:
simp [h, ih]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).drop.drop = ↑(drop ⟨is, h⟩)

Tactic:
by simp [assocRight, drop, cast_type, List.drop_drop]

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑(i + 1) + 1) * fib (-↑(i + 1) - 1) - fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs

Tactic:
show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp,

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑i) * fib (-↑(i + 1) - 1) - fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit 0 = b

Tactic:
rw [bit_negSucc]

Goal state after:
b : Bool
n : ℕ
⊢ -[Nat.bit (!b) n+1].testBit 0 = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)

Tactic:
try {rfl}

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

Tactic:
try {rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

Tactic:
try {rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]

Tactic:
try {rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)

Tactic:
try {rfl}

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

Tactic:
try {rfl}

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

Tactic:
try {rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]

Tactic:
try {rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

Tactic:
try {rfl}

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

Tactic:
try {rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

Tactic:
try {rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]

Tactic:
try {rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

Tactic:
try {rfl}

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

Tactic:
try {rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

Tactic:
try {rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]

Tactic:
try {rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ ↑(#(Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)) = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0

Tactic:
card_Ioc,

Goal state after:
a b r : ℤ
hr : 0 < r
⊢ ↑(⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋).toNat = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℕ
hr : 0 < r
v : ℕ
⊢ max (⌈(↑↑b - ↑↑v) / ↑↑r⌉ - ⌈(↑↑a - ↑↑v) / ↑↑r⌉) 0 = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0

Tactic:
Int.cast_natCast

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℕ
hr : 0 < r
v : ℕ
⊢ max (⌊(↑↑b - ↑↑v) / ↑↑r⌋ - ⌊(↑↑a - ↑↑v) / ↑↑r⌋) 0 = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0

Tactic:
Int.cast_natCast

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ ↑n.properDivisors
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
⊢ k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
refine ⟨_, ?_, prod_factorization_pow_eq_self hk⟩

Goal state after:
case neg.refine_1
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ ↑n.properDivisors
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
⊢ k.factorization < n.factorization
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k k' : ℕ
| X ^ k * ↑((n % p).choose k) * (X ^ (p * k') * ↑((n / p).choose k'))

Tactic:
rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]

Goal state after:
n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k k' : ℕ
| X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n

pp: case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌊/⌋ n

Tactic:
· obtain rfl | rfl := h <;> simp

Goal state after:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌊/⌋ n