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

Goal state before:

Tactic:
(f u) ^ p ≤ (c₁ * f x) ^ p := by
              exact rpow_le_rpow_of_nonpos (by positivity) (hf₁ u hu).1 (le_of_lt hp)
          _ = _ := by rw [← mul_rpow (le_of_lt hc₁_mem) (le_of_lt hf_pos)]

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
simp only [mod_two_ne_zero] at h

Goal state after:
case neg
m n : ℕ
h : (m + n) % 2 = 1
⊢ (m ^^^ n) % 2 = (m + n) % 2
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ ↑(Fin.ofNat 4 n) % 2 = 0

Tactic:
h

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ ↑0 % 2 = 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (↑(Fin.ofNat 4 n) % 2 + 1 % 2) % 2 = 0

Tactic:
h

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (↑1 % 2 + 1 % 2) % 2 = 0
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ e.decode (e.encode x✝¹) = e.decode (e.encode x✝)

Tactic:
h

Goal state after:
α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ e.decode (e.encode x✝) = e.decode (e.encode x✝)
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ some x✝¹ = some x✝

Tactic:
rw [← e.decode_encode, ← e.decode_encode, h]

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

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

Tactic:
induction m with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_ <;>
    intro n <;> 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

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

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.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ (∃ i, l[i]? = some (some x)) ↔ ∃ i, l.reduceOption[i]? = some x

Tactic:
by
  rw [← mem_iff_getElem?, ← mem_iff_getElem?, reduceOption_mem_iff]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
h : s ∈ M.εClosure S
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}

Tactic:
induction h with

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []

Tactic:
apply mem_εClosure_iff_exists

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet {start} (a :: s) = {List.foldl M.step start (a :: s)}

Tactic:
List.foldl,

Goal state after:
case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet (M.toNFA.stepSet {start} a) s = {List.foldl M.step start (a :: s)}
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet (M.toNFA.stepSet {start} a) s = {List.foldl M.step start (a :: s)}

Tactic:
List.foldl,

Goal state after:
case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet (M.toNFA.stepSet {start} a) s = {List.foldl M.step (M.step start a) s}
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1

Tactic:
erw [ofNat'_bit true n, ofNat'_bit]
      simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₂ ∈ M.εClosure {s₁}
⊢ ∃ n, M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
induction h with

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

Goal state before:
pp: m n : PosNum
h : ↑m = ↑n
⊢ ↑↑m = ↑↑n

Tactic:
h

Goal state after:
m n : PosNum
h : ↑m = ↑n
⊢ ↑↑n = ↑↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a + b + c = a + (b + c)

Tactic:
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))]))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a + b = b + a

Tactic:
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))]))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a * b * c = a * (b * c)

Tactic:
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))]))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), 1 * a = a

Tactic:
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))]))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a * 1 = a

Tactic:
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))]))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a * b = b * a

Tactic:
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))]))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), (a + b) * c = a * c + b * c

Tactic:
transfer; simp [mul_add, mul_comm]

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a ≤ a

Tactic:
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))]))

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: 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 x : ℕ
⊢ (x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n) → x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
h

Goal state after:
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 x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b c : σ
h : f a = f b
⊢ (∃ b_1 ∈ f b, ReflTransGen (fun a b ↦ b ∈ f a) b_1 c) ↔ ∃ b ∈ f a, ReflTransGen (fun a b ↦ b ∈ f a) b c

Tactic:
h

Goal state after:
σ : Type u_1
f : σ → Option σ
a b c : σ
h : f a = f b
⊢ (∃ b_1 ∈ f b, ReflTransGen (fun a b ↦ b ∈ f a) b_1 c) ↔ ∃ b_1 ∈ f b, ReflTransGen (fun a b ↦ b ∈ f a) b_1 c
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_2.refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b ↦ b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ Sum.inr c✝ ∈ Part.some ((f a✝).elim (Sum.inl a✝) Sum.inr)

Tactic:
h

Goal state after:
case refine_2.refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b ↦ b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ Sum.inr c✝ ∈ Part.some ((some c✝).elim (Sum.inl a✝) Sum.inr)
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ (match none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ a₂ = none) ↔
    match none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none

Tactic:
h

Goal state after:
σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ (match none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ b₂ = none) ↔
    match none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case pair
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f✝ h✝ : ℕ →. ℕ
hf✝ : Nat.RecursiveIn O f✝
hh✝ : Nat.RecursiveIn O h✝
ihf : Nat.RecursiveIn O' f✝
ihg : Nat.RecursiveIn O' h✝
⊢ Nat.RecursiveIn O' fun n ↦ Nat.pair <$> f✝ n <*> h✝ n

Tactic:
| pair _ _ ihf ihg =>

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

Goal state before:
pp: 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 p a v 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

Tactic:
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
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: 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 p a v 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

Tactic:
h

Goal state after:
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.RegularExpressions

Goal state before:
pp: case h.left
α : 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
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: x = ((a :: t) :: S').flatten

Tactic:
simp [hs, hsum]

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

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ k)

Tactic:
h

Goal state after:
tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ tm.k₀)
Module: Mathlib.Computability.TuringMachine.Computable

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ k)

Tactic:
h

Goal state after:
tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ tm.k₁)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.get.refine_1
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
n : ℕ
⊢ ∃ c, ∀ (v : List.Vector ℕ n.succ), c.eval ↑v = pure <$> (↑fun v ↦ v.get 0) v

Tactic:
exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩

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

Goal state before:
pp: case rfind.mp
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
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
have := PFun.mem_fix_iff.1 h2

Goal state after:
case rfind.mp
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
this :
  (Sum.inl v' ∈
      (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))) ∨
    ∃ a',
      (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))) ∧
        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]
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
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
⊢ PreservesLimit (cospan f g) (toCompHausLike h)

Tactic:
by
  have : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesLimit _ (compHausLikeToTop _))
  exact preservesLimit_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

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

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ ∀ {X Y Z : CompHausLike P} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
by
    intro X Y Z f π hπ
    refine ⟨pullback f π, pullback.fst f π, ⟨⟨effectiveEpiStruct _ ?_⟩⟩, pullback.snd f π,
      (pullback.condition _ _).symm⟩
    intro y
    obtain ⟨z, hz⟩ := hs π hπ (f y)
    exact ⟨⟨(y, z), hz.symm⟩, 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)
⊢ i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π

Tactic:
rw [Iso.inv_comp_eq]

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 π)
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)
⊢ Sigma.desc π = i.hom ≫ finiteCoproduct.desc X π
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
⊢ TrCfg c₁ c₂ →
    match TM2.step M c₁ with
    | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) c₂ b₂
    | none => TM1.step (tr M) c₂ = none

Tactic:
h

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h : TrCfg c₁ c₂
⊢ match TM2.step M c₁ with
  | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) c₂ b₂
  | none => TM1.step (tr M) c₂ = none
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
Nat.cast_zero

Goal state after:
⊢ trNum 0 = []
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ IsOpen (g ⁻¹' Subtype.val ⁻¹' Z₂)

Tactic:
← isClosed_compl_iff,

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ IsClosed (g ⁻¹' Subtype.val ⁻¹' Z₂)ᶜ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
h : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
⊢ IsOpen (Sigma.mk i ⁻¹' closure s)

Tactic:
h

Goal state after:
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
h : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
⊢ IsOpen (closure (Sigma.mk i ⁻¹' s))