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

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m &&& n) = ↑m &&& ↑n

Tactic:
by
  apply castNum_eq_bitwise PosNum.land <;> intros <;> (try cases_type* Bool) <;> rfl

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

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  SupportsStmt S q₁ →
    (∀ q' ∈ writes q₁, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ :
  SupportsStmt S q₂ →
    (∀ q' ∈ writes q₂, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
replace IH₁ := IH₁ hs.1 fun q hq ↦ hw q (Or.inl hq)

Goal state after:
case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₂ :
  SupportsStmt S q₂ →
    (∀ q' ∈ writes q₂, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
IH₁ : SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₂ :
  SupportsStmt S q₂ →
    (∀ q' ∈ writes q₂, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
IH₁ : SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
replace IH₂ := IH₂ hs.2 fun q hq ↦ hw q (Or.inr hq)

Goal state after:
case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
IH₁ : SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ : SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.prec.succ.succ
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))
b : ℕ
IH :
  ∀ (a : ℕ),
    a + b = n →
      n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
        PFun.fix
          (fun v ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a :: b :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)
a : ℕ
e : a + (b + 1) = n
⊢ n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
    PFun.fix
      (fun v ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (a :: (b + 1) :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)

Tactic:
refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl

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

Goal state before:
pp: case pos
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v ↦
              (cf.eval v).bind fun y ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
simp only [List.headI_cons, exists_false, or_false, Part.mem_some_iff,
          List.tail_cons, false_and, Sum.inl.injEq, reduceCtorEq] at this

Goal state after:
case pos
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
this : v' = n.succ :: ↑v
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case rfind.mpr.succ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
w : List ℕ
n : ℕ
IH :
  (∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0) →
    w ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (n :: ↑v) →
      w ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: ↑v)
hm : ∀ {m : ℕ}, m < n + 1 → ¬f (m ::ᵥ v) = 0
this :
  w ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      ((n + 1) :: ↑v)
⊢ w ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)

Tactic:
refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
        simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false,
          Part.mem_some_iff, List.tail_cons]

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

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ : CompHausLike P
⊢ ∀ {Y Z : CompHausLike P} (f : Z ⟶ X✝ ⨿ Y), HasExplicitPullback coprod.inl f

Tactic:
_

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ : CompHausLike P
⊢ ∀ {Z : CompHausLike P} (f : Z ⟶ X✝ ⨿ Y✝), HasExplicitPullback coprod.inl f
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ : CompHausLike P
⊢ ∀ {Z : CompHausLike P} (f : Z ⟶ X✝ ⨿ Y✝), HasExplicitPullback coprod.inl f

Tactic:
_

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ Z✝ : CompHausLike P
⊢ ∀ (f : Z✝ ⟶ X✝ ⨿ Y✝), HasExplicitPullback coprod.inl f
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_1
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt S q →
        (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (stRun s q) →
        (∀ x ∈ trStmts₁ (stRun s q), x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q)) ∧
            ∀ l' ∈ trStmts₁ (stRun s q), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
_

Goal state after:
case refine_1
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
⊢ (TM2.SupportsStmt S q✝ →
      (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')) →
    TM2.SupportsStmt S (stRun s q✝) →
      (∀ x ∈ trStmts₁ (stRun s q✝), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
          ∀ l' ∈ trStmts₁ (stRun s q✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_2
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
a✝ : σ → σ
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt S q →
        (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (TM2.Stmt.load a✝ q) →
        (∀ x ∈ trStmts₁ (TM2.Stmt.load a✝ q), x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q)) ∧
            ∀ l' ∈ trStmts₁ (TM2.Stmt.load a✝ q), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
_

Goal state after:
case refine_2
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
a✝ : σ → σ
q✝ : TM2.Stmt Γ Λ σ
⊢ (TM2.SupportsStmt S q✝ →
      (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')) →
    TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝) →
      (∀ x ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
          ∀ l' ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
⊢ ∀ (q₁ q₂ : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt S q₁ →
        (∀ x ∈ trStmts₁ q₁, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q₁) ∧ ∀ l' ∈ trStmts₁ q₁, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      (TM2.SupportsStmt S q₂ →
          (∀ x ∈ trStmts₁ q₂, x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal q₂) ∧ ∀ l' ∈ trStmts₁ q₂, TM1.SupportsStmt (trSupp M S) (tr M l')) →
        TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁ q₂) →
          (∀ x ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁ q₂), x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁ q₂)) ∧
              ∀ l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁ q₂), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
_

Goal state after:
case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ : TM2.Stmt Γ Λ σ
⊢ ∀ (q₂ : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt S q₁✝ →
        (∀ x ∈ trStmts₁ q₁✝, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧ ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      (TM2.SupportsStmt S q₂ →
          (∀ x ∈ trStmts₁ q₂, x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal q₂) ∧ ∀ l' ∈ trStmts₁ q₂, TM1.SupportsStmt (trSupp M S) (tr M l')) →
        TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂) →
          (∀ x ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂), x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂)) ∧
              ∀ l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ : TM2.Stmt Γ Λ σ
⊢ ∀ (q₂ : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt S q₁✝ →
        (∀ x ∈ trStmts₁ q₁✝, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧ ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      (TM2.SupportsStmt S q₂ →
          (∀ x ∈ trStmts₁ q₂, x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal q₂) ∧ ∀ l' ∈ trStmts₁ q₂, TM1.SupportsStmt (trSupp M S) (tr M l')) →
        TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂) →
          (∀ x ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂), x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂)) ∧
              ∀ l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
_

Goal state after:
case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : TM2.Stmt Γ Λ σ
⊢ (TM2.SupportsStmt S q₁✝ →
      (∀ x ∈ trStmts₁ q₁✝, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧ ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')) →
    (TM2.SupportsStmt S q₂✝ →
        (∀ x ∈ trStmts₁ q₂✝, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧ ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝) →
        (∀ x ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝), x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
            ∀ l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
⊢ (∀ x ∈ trStmts₁ (TM2.Stmt.goto l✝), x ∈ trSupp M S) →
    TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
      ∀ l' ∈ trStmts₁ (TM2.Stmt.goto l✝), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
_

Goal state after:
case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ x ∈ trStmts₁ (TM2.Stmt.goto l✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ l' ∈ trStmts₁ (TM2.Stmt.goto l✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
x✝ : TM2.SupportsStmt S TM2.Stmt.halt
⊢ (∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S) →
    TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
      ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
_

Goal state after:
case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
    ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj
            { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
              prop := ⋯ }).map
        f ≫
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app k).hom =
    InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f

Tactic:
ext ⟨g, p⟩

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
g : (j : J) → ↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
p :
  g ∈
    {u |
      ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f)) (u i) = u j}
⊢ (ConcreteCategory.hom
        (((Functor.const J).obj
                { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
                  prop := ⋯ }).map
            f ≫
          InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app k).hom))
      ⟨g, p⟩ =
    (ConcreteCategory.hom
        (InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f))
      ⟨g, p⟩
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
⊢ x ∈ univ →
    ∀ ⦃y : X⦄,
      y ∈ univ → x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y

Tactic:
_

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝ : x ∈ univ
⊢ ∀ ⦃y : X⦄, y ∈ univ → x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝ : x ∈ univ
y : X
⊢ y ∈ univ → x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y

Tactic:
_

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
⊢ x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y
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_1 : TopologicalSpace C] [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C]
    {f : A → C} {g : B → C}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_

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] [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
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] [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_

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
⊢ ∀ [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f