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

Goal state before:
pp: case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k' + 1, cf) n).bind
      fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
rw [hg (Nat.pair_lt_pair_right _ lf)]

Goal state after:
case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((evaln k cf n).bind fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
n : PosNum
⊢ (one.cmp n).swap = n.cmp one

Tactic:
obtain - | n | n := n

Goal state after:
case one.one
⊢ (one.cmp one).swap = one.cmp one

case one.bit1
n : PosNum
⊢ (one.cmp n.bit1).swap = n.bit1.cmp one

case one.bit0
n : PosNum
⊢ (one.cmp n.bit0).swap = n.bit0.cmp one
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n).swap = n.cmp m.bit1

Tactic:
obtain - | n | n := n

Goal state after:
case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit1.cmp one).swap = one.cmp m.bit1

case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1

case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n).swap = n.cmp m.bit0

Tactic:
obtain - | n | n := n

Goal state after:
case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit0.cmp one).swap = one.cmp m.bit0

case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0

case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit1.cmp b.bit1) (↑a.bit1 < ↑b.bit1) (a.bit1 = b.bit1) (↑b.bit1 < ↑a.bit1)

Tactic:
dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)
    · rw [this]
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)

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

Goal state before:
pp: x✝² x✝¹ x✝ : Num
⊢ ↑(x✝² * x✝¹ * x✝) = ↑(x✝² * (x✝¹ * x✝))

Tactic:
mul_to_nat,

Goal state after:
x✝² x✝¹ x✝ : Num
⊢ ↑x✝² * ↑x✝¹ * ↑x✝ = ↑x✝² * (↑x✝¹ * ↑x✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝ : Num
⊢ ↑(1 * x✝) = ↑x✝

Tactic:
mul_to_nat,

Goal state after:
x✝ : Num
⊢ ↑1 * ↑x✝ = ↑x✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝ : Num
⊢ ↑(x✝ * 1) = ↑x✝

Tactic:
mul_to_nat,

Goal state after:
x✝ : Num
⊢ ↑x✝ * ↑1 = ↑x✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝ : Num
⊢ ↑(0 * x✝) = ↑0

Tactic:
mul_to_nat,

Goal state after:
x✝ : Num
⊢ ↑0 * ↑x✝ = ↑0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝ : Num
⊢ ↑(x✝ * 0) = ↑0

Tactic:
mul_to_nat,

Goal state after:
x✝ : Num
⊢ ↑x✝ * ↑0 = ↑0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝¹ x✝ : Num
⊢ ↑(x✝¹ * x✝) = ↑(x✝ * x✝¹)

Tactic:
mul_to_nat,

Goal state after:
x✝¹ x✝ : Num
⊢ ↑x✝¹ * ↑x✝ = ↑x✝ * ↑x✝¹
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ x',
      (∃ l₁ l₂, x' = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = x ∧ ∃ n, l₂ = List.replicate n none) ∧ M.IsPath s₁ s₂ x') →
    ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
intro ⟨_, ⟨x', _, rfl, _, n, rfl⟩, h⟩

Goal state after:
case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left✝ : x'.reduceOption = x
n : ℕ
h : M.IsPath s₁ s₂ (x' ++ some a :: List.replicate n none)
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
m n : PosNum
⊢ ↑↑(m * n) = ↑m * ↑n

Tactic:
mul_to_nat,

Goal state after:
α : Type u_1
inst✝ : NonAssocSemiring α
m n : PosNum
⊢ ↑(↑m * ↑n) = ↑m * ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ ↑(pos p).pred = (↑(pos p)).pred

Tactic:
by rw [pred, PosNum.pred'_to_nat]; rfl

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case inl
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

pp: case inr
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
· exact ⟨k, x, by simp [e]⟩

Goal state after:
case inr
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → Prop
hp : ComputablePred p
⊢ REPred p

Tactic:
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
  unfold REPred
  dsimp only
  refine
    (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n =>
      Part.ext fun a => ?_
  cases a; cases f n <;> simp

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
⊢ q ≤₁ (q ∘ ⇑e)

Tactic:
convert! OneOneReducible.of_equiv _ h; funext; simp

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

Goal state before:
pp: case right.some.some.branch
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.branch p q₁ q₂) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
cases h : p a v <;> rw [trAux, h] at h₁

Goal state after:
case right.some.some.branch.false
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (bif false then trAux M a q₁ v else trAux M a q₂ v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = false
⊢ some val✝ ∈ TM1.stmts M S

case right.some.some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (bif true then trAux M a q₁ v else trAux M a q₂ v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = true
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ trTape enc0 (Tape.mk' L R) = trTape' enc0 L R

Tactic:
by
  simp only [trTape, Tape.mk'_left, Tape.mk'_right₀]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : P.star.rmatch u = true
hwf : u.length < (a :: x).length
⊢ ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
IH _ hwf

Goal state after:
case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : ∃ S, u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hwf : u.length < (a :: x).length
⊢ ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ zero.eval v = pure [0]

Tactic:
by simp [zero]

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

Goal state before:
pp: case goto
Γ : 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
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
refine ⟨?_, fun _ ↦ False.elim⟩

Goal state after:
case goto
Γ : 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
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : 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
hs : SupportsStmt S Stmt.halt
hw : ∀ q' ∈ writes Stmt.halt, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
refine ⟨?_, fun _ ↦ False.elim⟩

Goal state after:
case halt
Γ : 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
hs : SupportsStmt S Stmt.halt
hw : ∀ q' ∈ writes Stmt.halt, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: k k' : Cont
v : List ℕ
⊢ (k.then k').eval v = k.eval v >>= k'.eval

Tactic:
by
  induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]

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
⊢ g = ofHom P (⋯.liftEquiv ⟨TopCat.Hom.hom e.hom, ⋯⟩)

Tactic:
apply ConcreteCategory.ext

Goal state after:
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
⊢ ConcreteCategory.hom g = ConcreteCategory.hom (ofHom P (⋯.liftEquiv ⟨TopCat.Hom.hom e.hom, ⋯⟩))
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
x✝ : Epi (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]

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

Goal state before:
pp: case neg
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)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
· obtain ⟨k₀, v₀, e₀⟩ := stepNormal.is_ret f Cont.halt v'.tail
        have e₁ := stepNormal_then f Cont.halt (Cont.fix f k) v'.tail
        rw [e₀, Cont.then, Cfg.then] at e₁
        simp only at e₁
        obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
          IH (stepRet (k₀.then (Cont.fix f k)) v₀) (by rw [stepRet, if_neg he, e₁]; rfl)
            v'.tail _ stepRet_then (by apply ReflTransGen.single; rw [e₀]; rfl)
        refine ⟨_, PFun.mem_fix_iff.2 ?_, h₃⟩
        simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]
        split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
          exact Or.inr ⟨_, rfl, hv₂⟩]

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

Goal state before:
pp: case some.nil
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o : α
h₁ : ∀ x ∈ [], p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], some o, l₂)

Tactic:
rcases h₂ with ⟨h₂, ⟨⟩⟩

Goal state after:
case some.nil
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ [], p x = false
h₂ : p a = true
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], some a, L)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case some.cons
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ : Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, some o, l₂)

Tactic:
rcases h₂ with ⟨h₂, ⟨⟩⟩

Goal state after:
case some.cons
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ (bif p a then ([], some a, l₁.append (o :: l₂))
    else
      match splitAtPred p (l₁.append (o :: l₂)) with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a :: l₁, some o, 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✝ : ∀ x ∈ trStmts₁ (TM2.Stmt.goto l✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
refine ⟨?_, fun _ ↦ False.elim⟩

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✝))
Module: Mathlib.Topology.Category.Profinite.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
x✝ : Epi (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]

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

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
x✝ : Epi (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mpr.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
e : J
he : e ∈ G
⊢ ⇑(ConcreteCategory.hom (F.map (g e he))) ⁻¹' U e ∈ T j

Tactic:
exact compat j e (g e he) (U e) (h1 e he)

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

Goal state before:
pp: f fs : Code
k : Cont'
⊢ codeSupp (f.cons fs) k = trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k)

Tactic:
by
  simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]

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

Goal state before:
pp: case fix.true
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif true then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

Tactic:
· exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)

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

Goal state before:
pp: case comp
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (f.comp g) k ⊆ S
⊢ Λ'.Supports S (trNormal g (Cont'.comp f k))

Tactic:
apply IHg; rw [codeSupp_comp] at Hk; exact Finset.union_subset_right Hk

Goal state after: