mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
k' : K'
s' : Option Γ' → Option Γ'
q' : Λ'
⊢ Decidable (push k s q = push k' s' q')

Tactic:
exact decidable_of_iff' (k = k' ∧ s = s' ∧ q = q') (by simp)

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ Reaches step (stepNormal f Cont.halt v'.tail) (stepRet k₀ v₀)

Tactic:
apply ReflTransGen.single

Goal state after:
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ stepRet k₀ v₀ ∈ step (stepNormal f Cont.halt v'.tail)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
let ρ : E → A := E.domRestrict X₁

Goal state after:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
Module: Mathlib.Condensed.Basic

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
S T : CompHausᵒᵖ
g : S ⟶ T
x : X.obj.obj S
⊢ (ConcreteCategory.hom (f.hom.app T)) ((ConcreteCategory.hom (X.obj.map g)) x) =
    (ConcreteCategory.hom (Y.obj.map g)) ((ConcreteCategory.hom (f.hom.app S)) x)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case case.succ
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step tr)
    { l := some ((trNormal f (trCont k)).pred (trNormal g (trCont k))), var := s,
      stk := elim (trList v) [] [] (trContStack k) }
    (Nat.rec { l := some (trNormal f (trCont k)), var := s', stk := elim (trList v.tail) [] [] (trContStack k) }
      (fun n x ↦
        { l := some (trNormal g (trCont k)), var := s', stk := elim (trList (n :: v.tail)) [] [] (trContStack k) })
      (n + 1))
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) (n + 1)) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IHg k _ s'

Goal state after:
case case.succ
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step tr)
    { l := some ((trNormal f (trCont k)).pred (trNormal g (trCont k))), var := s,
      stk := elim (trList v) [] [] (trContStack k) }
    (Nat.rec { l := some (trNormal f (trCont k)), var := s', stk := elim (trList v.tail) [] [] (trContStack k) }
      (fun n x ↦
        { l := some (trNormal g (trCont k)), var := s', stk := elim (trList (n :: v.tail)) [] [] (trContStack k) })
      (n + 1))
c : Cfg'
h₁ : TrCfg (stepNormal g k ?m.800) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal g (trCont k)), var := s', stk := elim (trList ?m.800) [] [] (trContStack k) } c
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) (n + 1)) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
Module: Mathlib.Condensed.Light.Basic

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
S T : LightProfiniteᵒᵖ
g : S ⟶ T
x : X.obj.obj S
⊢ (ConcreteCategory.hom (f.hom.app T)) ((ConcreteCategory.hom (X.obj.map g)) x) =
    (ConcreteCategory.hom (Y.obj.map g)) ((ConcreteCategory.hom (f.hom.app S)) x)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v) → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (TM2.step tr) i

Tactic:
simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff, Cfg.halt.injEq,
      exists_eq_right] at this

Goal state after:
case refine_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this : v' ∈ c.eval v → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (TM2.step tr) i
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ ↑↑x ∈ ↑(Fiber.mk f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b))

Tactic:
rw [Fiber.mem_iff_eq_image, Fiber.mk_image, this, ← Fiber.map_preimage_eq_image]

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ (f ∘ fun x ↦ ↑x) (Fiber.preimage (f ∘ fun x ↦ ↑x) b) = f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b)
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)
a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)
x : ↑↑a
⊢ ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (isTerminalPUnit.from
                    (fiber (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a)).hom)
              g }
        (Fiber.image (⇑(map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f)) a))
      x =
    ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (sigmaIncl (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a).hom)
              g }
        f)
      x

Tactic:
erw [← map_eq_image _ a 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)
x : ↑↑a
⊢ ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (isTerminalPUnit.from
                    (fiber (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a)).hom)
              g }
        ((map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) ↑x))
      x =
    ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (sigmaIncl (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a).hom)
              g }
        f)
      x
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
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
isSheaf_iff_preservesFiniteProducts_of_projective F

Goal state after:
A : Type u_1
inst✝² : Category.{v_1, u_1} A
inst✝¹ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
⊢ PreservesFiniteProducts F
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
⊢ IsSheaf (coherentTopology Profinite) F

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F

Goal state after:
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
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
⊢ IsSheaf (coherentTopology CompHaus) F

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
F : CompHausᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F
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ᵒᵖ) (xi : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i))
    (xj : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj

Tactic:
intro ⟨i⟩

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 : I
⊢ ∀ (j : Iᵒᵖ) (xi : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i)))
    (xj : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj
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ᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (toProfinite.op.obj Y) ≫ X.map g

Tactic:
simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]

Goal state after:
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✝
⊢ ((↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv) ≫ X.map g =
    (counitApp X).app (Opposite.op (toProfinite.obj (Opposite.unop Y))) ≫ X.map g
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
⊢ IsSheaf (coherentTopology LightProfinite) F

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
F : LightProfiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F
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 : ℕᵒᵖᵒᵖ) (xi : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i))
    (xj : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj

Tactic:
intro ⟨i⟩

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 : ℕᵒᵖᵒᵖ) (xi : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i)))
    (xj : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj
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ᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (toLightProfinite.op.obj Y) ≫ X.map g

Tactic:
simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]

Goal state after:
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✝
⊢ ((↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv) ≫ X.map g =
    (counitApp X).app (Opposite.op (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
⊢ ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) g

Tactic:
refine ⟨S', π, hπ, (ihomPoints _ _ _ _).symm g', ?_⟩

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
⊢ (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) ((ihomPoints R P A S').symm g') =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) g
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))

Tactic:
by cases x; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))

Tactic:
by cases x; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = mk fun s ↦ goto x (i, s)

Tactic:
by cases x; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)

Tactic:
by cases x; rfl

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) f) = f

Tactic:
by cases f <;> simp [Except.map]

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) f) = f

Tactic:
by cases f <;> simp [Except.map]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = g (Part.fix g)

Tactic:
fix_eq_ωSup_of_ωScottContinuous hc,

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) = g (ωSup (approxChain { toFun := g, monotone' := ⋯ }))
Module: Mathlib.Data.BitVec

Goal state before:
pp: case zero
z : ℤ
⊢ { toFin := ↑z } = ↑z

pp: case succ
z : ℤ
n✝ : ℕ
⊢ { toFin := ↑z } = ↑z

Tactic:
case zero =>
    simp only [eq_nil]

Goal state after:
case succ
z : ℤ
n✝ : ℕ
⊢ { toFin := ↑z } = ↑z
Module: Mathlib.Data.Bool.AllAny

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (l.all fun a ↦ decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a

Tactic:
by
  simp

Goal state after:
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 ι
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
let := Classical.decEq ι

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 ι
⊢ Infinite (Π₀ (i : ι), π i)
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ 2 * count b l = count b l + count b l

Tactic:
two_mul

Goal state after:
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ count b l + count b l = count b l + count b l
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ #f.pi = f.prod fun i ↦ ↑(#(f i))

Tactic:
rw [pi, card_dfinsupp]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i ↦ ↑(#(f i))
Module: Mathlib.Data.FP.Basic

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

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

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
⊢ ∀ (x : Sigma β), x ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)

Tactic:
intro x; cases x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt8.ofFin UInt8.toFin

Tactic:
intro x; simp

Goal state after: