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

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso ((LightCondensed.forget R).map ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)))

Tactic:
dsimp [LightCondensed.forget, discreteUnderlyingAdj]
  rw [← constantSheafAdj_counit_w]
  refine IsIso.comp_isIso' inferInstance ?_
  have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Faithful :=
    inferInstanceAs (discrete _).Faithful
  have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Full :=
    inferInstanceAs (discrete (Type u)).Full
  rw [← Sheaf.isConstant_iff_isIso_counit_app]
  constructor
  change (discrete _).essImage _
  rw [essImage_eq_of_natIso LightCondSet.LocallyConstant.iso.symm]
  exact obj_mem_essImage LightCondSet.LocallyConstant.functor M

Goal state after:
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(hom (f.hom.app (op S.compHaus)))

Tactic:
rw [← (StoneanCompHaus.equivalence A).inverse.epi_map_iff_epi,
    ← Presheaf.coherentExtensiveEquivalence.functor.epi_map_iff_epi,
    ← isLocallySurjective_iff_epi']
  exact extensiveTopology.isLocallySurjective_iff (D := A) _

Goal state after:
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 Stonean.toCompHaus.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✝¹ : ReflectsFiniteProducts (CategoryTheory.forget A)
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology Stonean) (F ⋙ CategoryTheory.forget A)

Tactic:
isSheaf_iff_preservesFiniteProducts_of_projective

Goal state after:
A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.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✝¹ : ReflectsFiniteProducts (CategoryTheory.forget A)
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
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✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝) =
    (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✝)

Tactic:
simp only [← assoc]

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝) =
    (((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.Discrete.Colimit

Goal state before:
pp: case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
⊢ ∃ k f g,
    (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
      (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj

Tactic:
refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩

Goal state after:
case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
⊢ (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map ki.op)) fi =
    (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map kj.op)) fj
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
⊢ ∃ k f g,
    (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
      (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj

Tactic:
refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
⊢ (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map ki.op)) fi =
    (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map kj.op)) fj
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
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
obtain ⟨C, C_clopen, Z_subset_C, C_subset_D, C_cover_D, C_disj⟩ :=
    exists_clopen_partition_of_clopen_cover Z_closed D_clopen Z_subset_D Z_disj

Goal state after:
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 : univ.PairwiseDisjoint C
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = 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 (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

Tactic:
simp only [← assoc]

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.Control.Bitraversable.Instances

Goal state before:
pp: case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
fst✝ : α✝
snd✝ : β✝
⊢ bitraverse pure pure (fst✝, snd✝) = pure (fst✝, snd✝)

Tactic:
simp [bitraverse, Prod.bitraverse, functor_norm]

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

Goal state before:
pp: case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) (fst✝, snd✝) =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ (fst✝, snd✝))

Tactic:
simp [bitraverse, Prod.bitraverse, functor_norm]

Goal state after:
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ Functor.Comp.mk ((fun a ↦ (fun x2 ↦ Prod.mk <$> f✝ a <*> x2) ∘ f'✝) <$> g✝ fst✝ <*> g'✝ snd✝) =
    Functor.Comp.mk ((fun a ↦ Prod.bitraverse f✝ f'✝ ∘ Prod.mk a) <$> g✝ fst✝ <*> g'✝ snd✝)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (fst✝, snd✝) = pure (bimap f✝ f'✝ (fst✝, snd✝))

Tactic:
simp [bitraverse, Prod.bitraverse, functor_norm]

Goal state after:
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ pure (f✝ fst✝, f'✝ snd✝) = pure (bimap f✝ f'✝ (fst✝, snd✝))
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ (fst✝, snd✝)) =
    bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) (fst✝, snd✝)

Tactic:
simp [bitraverse, Prod.bitraverse, functor_norm]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ InternallyProjective ((free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e

Tactic:
free_internallyProjective_iff_tensor_condition'

Goal state after:
R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ (∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite)
      (g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g = g' ≫ e) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.3
⊢ ⇑(Equiv.refl α).uniqueCongr = id

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: ⊢ ∀ {α β γ : Type ?u.3} (k : α ≃ β) (h : β ≃ γ), ⇑(k.trans h).uniqueCongr = ⇑h.uniqueCongr ∘ ⇑k.uniqueCongr

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type ?u.4
x✝ : Fintype α
⊢ Fintype.ofBijective ⇑(Equiv.refl α) ⋯ = id x✝

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: ⊢ ∀ {α β γ : Type ?u.4} (k : α ≃ β) (h : β ≃ γ),
    (fun x ↦ Fintype.ofBijective ⇑(k.trans h) ⋯) = (fun x ↦ Fintype.ofBijective ⇑h ⋯) ∘ fun x ↦ Fintype.ofBijective ⇑k ⋯

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = (fun x1 x2 ↦ x1 ++ x2) <$> traverse f (a :: as) <*> traverse f bs

Tactic:
simp [traverse_append as bs, functor_norm]

Goal state after:
F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (fun a ↦ (Function.comp fun x2 ↦ a :: x2) ∘ fun x1 x2 ↦ x1 ++ x2) <$> f a <*> traverse f as <*> traverse f bs =
    (fun a ↦ (fun x1 x2 ↦ x1 ++ x2) ∘ fun x2 ↦ a :: x2) <$> f a <*> traverse f as <*> traverse f bs
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 ↦ x)

Tactic:
ext i : 1; cases i <;> rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
⊢ α.repeatEq = nilFun

Tactic:
by ext i; cases i

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X

Tactic:
intro i

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
i : ℕ
⊢ { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ approxChain { toFun := g, monotone' := ⋯ } ≤
    (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }

Tactic:
intro i

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ j,
    (approxChain { toFun := g, monotone' := ⋯ }) i ≤
      ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) j
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ } ≤
    approxChain { toFun := g, monotone' := ⋯ }

Tactic:
intro i

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ j,
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i ≤
      (approxChain { toFun := g, monotone' := ⋯ }) j
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 ι
this : DecidableEq ι := Classical.decEq ι
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
choose m hm using fun i => exists_ne (0 : π i)

Goal state after:
ι✝ : 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 ι
this : DecidableEq ι := Classical.decEq ι
m : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ 0
⊢ Infinite (Π₀ (i : ι), π i)
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ (toDFinsupp (replicate n a)) i = (DFinsupp.single a n) i

Tactic:
dsimp [toDFinsupp]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = (DFinsupp.single a n) i
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s

Tactic:
refine ⟨congr_arg _, fun h => ?_⟩

Goal state after:
α : Type u_1
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries

Tactic:
simp only [union_entries, Option.mem_def, dlookup_kunion_eq_some]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝ ↔
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), lookup x ⟦s₁⟧ = lookup x ⟦s₂⟧
⊢ ⟦s₁⟧ = ⟦s₂⟧

Tactic:
simp only [AList.lookup, lookup_toFinmap] at h

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ⟦s₁⟧ = ⟦s₂⟧
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ && (f x✝² x✝¹ && f x✝ b₂)) = (x✝³ && (f x✝ b₂ && f x✝² x✝¹))

Tactic:
Bool.and_comm,

Goal state after:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), True
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Tactic:
· rw [lookup_union_left h']

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)

Tactic:
by_cases x = y.1

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)

case neg
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : ¬x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
nd₁ : [].NodupKeys
nd₂ : l₂.NodupKeys
⊢ ([].kunion l₂).NodupKeys

Tactic:
simp only [nil_kunion, nd₂]

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

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

Tactic:
intro i

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

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

Tactic:
intro i

Goal state after:
case hn
m n i : ℕ
⊢ ∀ (m : ℕ), -[i+1].bodd = (m.bodd ^^ (m + i + 1).bodd)
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
rw [Nat.bitwise_swap, Function.swap]

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

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && y) m n) = -[m+1].land (ofNat n)

Tactic:
rw [Nat.bitwise_swap, Function.swap]

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && y) n m) = -[m+1].land (ofNat n)
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
rw [Nat.bitwise_swap, Function.swap]

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && !!y) n m) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)