mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.false
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit false n✝) = bit (true != false) (bif false != true then pos n✝ else 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.true
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit true n✝) = bit (true != true) (bif false != true then pos n✝ else 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).lxor 1 = bit (false != true) (bif true != false then pos m✝ else 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).lxor 1 = bit (true != true) (bif true != false then pos m✝ else 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit false n✝) = bit (false != false) (m✝.lxor n✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit true n✝) = bit (false != true) (m✝.lxor n✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit false n✝) = bit (true != false) (m✝.lxor n✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit true n✝) = bit (true != true) (m✝.lxor n✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero
a✝ : PosNum
⊢ ↑(a✝ <<< 0) = ↑a✝ <<< 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.one
⊢ ↑(one >>> 0) = ↑(pos one) >>> 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.bit1
a✝ : PosNum
⊢ ↑(a✝.bit1 >>> 0) = ↑(pos a✝.bit1) >>> 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.bit0
a✝ : PosNum
⊢ ↑(a✝.bit0 >>> 0) = ↑(pos a✝.bit0) >>> 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.one
⊢ true = (↑one).testBit 0

Tactic:
rfl

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

Goal state before:
pp: case move
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Dir
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.move a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
rfl

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

Goal state before:
pp: case write
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Γ
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.write a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.write a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
rfl

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

Goal state before:
pp: case prim.prec.succ.zero
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
a : ℕ
e : a + 0 = n
⊢ Part.some
      (if (0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI = 0 then
        Sum.inl
          ((a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
            (0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.pred ::
              [g
                      ((a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::ᵥ
                        Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ v.tail)].headI ::
                (↑v).tail)
      else
        Sum.inr
          ((a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
            (0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.pred ::
              [g
                      ((a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::ᵥ
                        Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ v.tail)].headI ::
                (↑v).tail)) =
    Part.some
      (Sum.inl
        ((a + 0).succ ::
          0 :: g ((a + 0) ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) (a + 0) ::ᵥ v.tail) :: (↑v).tail))

Tactic:
rfl

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

Goal state before:
pp: case right.e_a.e_a.nil
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
e : S k = []
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))).head.2 k = [].head?

Tactic:
rfl

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

Goal state before:
pp: case right.e_a.e_a.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ some head✝ = (head✝ :: tail✝).head?

Tactic:
rfl

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

Goal state before:
pp: case pos
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
⊢ none = default

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ Function.Injective ⇑(ConcreteCategory.hom (ι X a))

Tactic:
intro x y hxy
  exact eq_of_heq (Sigma.ext_iff.mp hxy).2

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P✝¹ : TopCat → Prop
α : Type w
inst✝³ : Finite α
X : α → CompHausLike P✝¹
inst✝² : HasExplicitFiniteCoproduct X
P✝ : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P✝
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
⊢ PreservesFiniteCoproducts (compHausLikeToTop P)

Tactic:
refine ⟨fun n ↦ ⟨fun {F} ↦ ?_⟩⟩
  suffices PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P) from
    preservesColimit_of_iso_diagram _ Discrete.natIsoFunctor.symm
  exact preservesColimit_of_preserves_colimit_cocone (CompHausLike.finiteCoproduct.isColimit _)
    ((isColimitMapCoconeCofanMkEquiv _ _ _).2 (TopCat.sigmaCofanIsColimit _))

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

Goal state before:
pp: case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
h✝ : v.headI = 0
⊢ a✝.eval v.tail >>= k'.eval = a✝.eval v.tail >>= k'.eval

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
⊢ cospan f.hom g.hom ≅
    cospan ((cospan f g ⋙ compHausLikeToTop P).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ compHausLikeToTop P).map WalkingCospan.Hom.inr)

Tactic:
rfl

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

Goal state before:
pp: case zero
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
H : 0 ≤ S.length
⊢ Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
    { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[0] (Tape.mk' ∅ (addBottom L)) }

Tactic:
rfl

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

Goal state before:
pp: case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = stepNormal a✝² ((Cont.cons₂ v a✝).then k') a✝¹

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
B X : CompHausLike P
π : X ⟶ B
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
W✝ : CompHausLike P
e : X ⟶ W✝
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a✝ : (fun X ↦ ↑X.toTop) X
⊢ (ConcreteCategory.hom g) ((ConcreteCategory.hom π) a✝) = (TopCat.Hom.hom (π ≫ g).hom) a✝

Tactic:
rfl

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

Goal state before:
pp: case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = stepNormal a✝¹ ((Cont.fix a✝¹ a✝).then k') v.tail

Tactic:
rfl

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  n ≤ S.length →
    Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
      { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
H : n + 1 ≤ S.length
⊢ some
      (bif (some S.reverse[n]).isNone then
        TM1.stepAux (trStAct (goto fun x x_1 ↦ ret q) o) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))
      else
        { l := some (go k o q), var := v,
          Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }) =
    some
      { l := some (go k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }

Tactic:
rfl

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

Goal state before:
pp: case zero
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[0] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }

Tactic:
rfl

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then
      TM1.stepAux (trNormal q) v (Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))))
    else TM1.stepAux (goto fun x x_1 ↦ ret q) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
⊢ t = (ConcreteCategory.hom (𝟙 (∐ X))) t

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this✝ : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (finiteCoproduct.desc X π)) ((ConcreteCategory.hom i.hom) t)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
a : α
a✝ : ↑(X a).toTop
⊢ (ConcreteCategory.hom (π a)) a✝ = (ConcreteCategory.hom (finiteCoproduct.ι X a ≫ finiteCoproduct.desc X π)) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE

Tactic:
tfae_have 2 → 3
  | e => by
    rw [epi_iff_surjective] at e
    let i : ∐ X ≅ finiteCoproduct X :=
      (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _)
    intro b
    obtain ⟨t, rfl⟩ := e b
    let q := i.hom t
    refine ⟨q.1,q.2,?_⟩
    have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id]; rfl
    rw [this]
    change _ = (i.inv ≫ Sigma.desc π) (i.hom t)
    suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by
      rw [this]; rfl
    rw [Iso.inv_comp_eq]
    apply colimit.hom_ext
    rintro ⟨a⟩
    simp only [i, Discrete.functor_obj, colimit.ι_desc, Cofan.mk_ι_app,
      colimit.comp_coconePointUniqueUpToIso_hom_assoc]
    ext; rfl

Goal state after:
α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: ⊢ trNum 0 = []

Tactic:
rfl

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

Goal state before:
pp: case main
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' main = elim a' b c d main

Tactic:
rfl

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

Goal state before:
pp: case rev
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' rev = elim a' b c d rev

Tactic:
rfl

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

Goal state before:
pp: case aux
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' aux = elim a' b c d aux

Tactic:
rfl

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

Goal state before:
pp: case stack
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' stack = elim a' b c d stack

Tactic:
rfl

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

Goal state before:
pp: case main
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' main = elim a b' c d main

Tactic:
rfl

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

Goal state before:
pp: case rev
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' rev = elim a b' c d rev

Tactic:
rfl

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

Goal state before:
pp: case aux
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' aux = elim a b' c d aux

Tactic:
rfl

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

Goal state before:
pp: case stack
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' stack = elim a b' c d stack

Tactic:
rfl

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

Goal state before:
pp: case main
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' main = elim a b c' d main

Tactic:
rfl

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

Goal state before:
pp: case rev
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' rev = elim a b c' d rev

Tactic:
rfl

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

Goal state before:
pp: case aux
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' aux = elim a b c' d aux

Tactic:
rfl

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

Goal state before:
pp: case stack
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' stack = elim a b c' d stack

Tactic:
rfl

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

Goal state before:
pp: case main
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' main = elim a b c d' main

Tactic:
rfl

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

Goal state before:
pp: case rev
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' rev = elim a b c d' rev

Tactic:
rfl

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

Goal state before:
pp: case aux
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' aux = elim a b c d' aux

Tactic:
rfl

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

Goal state before:
pp: case stack
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' stack = elim a b c d' stack

Tactic:
rfl

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₀
⊢ step (Cfg.ret (k₀.then (Cont.fix f k)) v₀) = some (stepRet (k₀.then (Cont.fix f k)) v₀)

Tactic:
rfl

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₀
⊢ stepRet k₀ v₀ ∈ step (Cfg.ret k₀ v₀)

Tactic:
rfl

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

Goal state before:
pp: case neg.none
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
⊢ (Option.map (fun a ↦ default k') none).getD default = [][i]?.getD default

Tactic:
rfl

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

Goal state before:
pp: case neg.some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
val✝ : Γ k
⊢ (Option.map (fun a ↦ default k') (some val✝)).getD default = [][i]?.getD default

Tactic:
rfl

Goal state after: