mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
⊢ (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 CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
congr 1

Goal state after:
case e_a
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) =
    ((functorIsoDiscreteAux₂ R X✝).inv ≫
        (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom
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:
congr 1

Goal state after:
case e_a
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)) =
    ((functorIsoDiscreteAux₂ R X✝).inv ≫
        (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map
          ((Functor.const LightProfiniteᵒᵖ).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom
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
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ toProfinite.map (F.map ki))) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ toProfinite.map (F.map kj))) x)

Tactic:
dsimp% c.w,

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
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app i)) x) = fj ((ConcreteCategory.hom (c.π.app k ≫ toProfinite.map (F.map kj))) x)
Module: Mathlib.Condensed.Discrete.Colimit

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

Tactic:
have : Finite (fiber.{u, u + 1} f x) :=
    Finite.of_injective (sigmaIncl.{u, u + 1} f x).1 Subtype.val_injective

Goal state after:
case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (CompHausLike.isTerminalPUnit.from (fiber f x)).op)) (Function.Fiber.image (⇑f) x)
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
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ toLightProfinite.map (F.map ki))) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ toLightProfinite.map (F.map kj))) x)

Tactic:
dsimp% c.w,

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
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app i)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ toLightProfinite.map (F.map kj))) x)
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: case h
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (Opposite.op 0))

Tactic:
simp only [LightProfinite.effectiveEpi_iff_surjective]

Goal state after:
case h
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (G.map (homOfLE ⋯).op))) →
      Function.Surjective ⇑(ConcreteCategory.hom (limit.π G (Opposite.op 0)))
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
⊢ Continuous ⇑(ConcreteCategory.hom f)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
⊢ Continuous ⇑(ConcreteCategory.hom g)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
⊢ Continuous ⇑(ConcreteCategory.hom g')

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

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

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  intro X
  exact inferInstanceAs (IsIso (compactlyGeneratedAdjunctionCounitIso X).hom)

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

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x

Tactic:
congr 1

Goal state after:
case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ Comp.instApplicativeComp = inst✝¹
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x

Tactic:
congr 1

Goal state after:
case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst✝¹
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 G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (traverse (pure ∘ f✝)) (traverse (pure ∘ f'✝)) x✝ = pure (bimap (Functor.map f✝) (Functor.map f'✝) x✝)

pp: case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ η✝.app (bicompl t F G β✝ β'✝) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (η✝.app β✝ ∘ f✝)) (traverse (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
· simp [traverse_eq_map_id', bitraverse_eq_bimap_id]

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ η✝.app (bicompl t F G β✝ β'✝) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (η✝.app β✝ ∘ f✝)) (traverse (η✝.app β'✝ ∘ f'✝)) x✝
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b

Tactic:
skip

Goal state after:
case pos.mpr.inr.inl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case refl.refl
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
fs : Fin2.elim0 ⟹ Fin2.elim0
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 Fin2.elim0 fs

Tactic:
cases eq₃

Goal state after:
case refl.refl.refl
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 Fin2.elim0 nilFun
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightProfinite
y : ↑Y.toTop
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom f)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
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
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : (π (σ (Option.some i) s)).2 = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x

Tactic:
hσ'

Goal state after:
case refine_2
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
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x
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
π : T → S × OnePoint X
hπ : Continuous π
⊢ Continuous Subtype.val

Tactic:
by fun_prop

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 π
x : OnePoint X
⊢ Continuous (Prod.snd ∘ π)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
⊢ (↑z).toFin = ↑z

Tactic:
← ofFin_intCast

Goal state after:
w : ℕ
z : ℤ
⊢ { toFin := ↑z }.toFin = ↑z
Module: Mathlib.Data.BitVec

Goal state before:
pp: w n : ℕ
x : BitVec w
⊢ (↑n).toFin * x.toFin = n • x.toFin

Tactic:
simp only [natCast_eq_ofNat, toFin_ofNat, Fin.ofNat_eq_cast, nsmul_eq_mul]

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

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

Tactic:
by fun_prop

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

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

Tactic:
by fun_prop

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

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

Tactic:
by fun_prop

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

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

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a : α
h : ∃ a_1, (fun x ↦ a_1 = x) = ↑(mk a) := (mk a).property
this : (fun x ↦ Classical.choose h = x) = ↑(mk a)
⊢ Classical.choose h = a

Tactic:
exact cast (congr_fun this a).symm rfl

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

Goal state before:
pp: n k : ℕ
h : k = 2 ^ n
a b c : Fin k
⊢ a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

Tactic:
grind [Fin.xor_val, Nat.xor_mod_two_pow, Nat.mod_mod]

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

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

Tactic:
by fun_prop

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

Goal state before:
pp: case succ.last
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ take (m + 1).succ h v (last (m + 1)) = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) (last (m + 1))

Tactic:
simp [take, snoc]; congr

Goal state after:
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty = congr x✝ inst✝ ⋯ empty

Tactic:
congr 1

Goal state after:
case h_1.e_x
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ pempty = x✝