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

Goal state before:
pp: case h₁
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ c₁ * f x ≤ f u

pp: case h₂
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ c₃ * g x ≤ g u

Tactic:
· exact (hf u hu).1

Goal state after:
case h₂
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ c₃ * g x ≤ g u
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x✝ : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x✝
hxr : ∃ r ∈ g.rules, Symbol.nonterminal r.input = Symbol.nonterminal t
⊢ ¬g.Derives x✝ s

Tactic:
Symbol.nonterminal.injEq

Goal state after:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x✝ : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x✝
hxr : ∃ r ∈ g.rules, r.input = t
⊢ ¬g.Derives x✝ s
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hpr
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
⊢ Primrec fun p ↦ Option.map (Nat.pair p.2) (lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1) p.1.1.1.2)

Tactic:
refine Primrec.option_map ((hlup.comp <| L.pair <| (k.pair cg).pair n).comp Primrec.fst) ?_

Goal state after:
case hpr
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
⊢ Primrec₂ fun p ↦ Nat.pair p.2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n ↦ 1 + ε ↑n) ~[atTop] fun n ↦ 1

Tactic:
rw [Function.const_def, isEquivalent_const_iff_tendsto one_ne_zero,
        ← Function.comp_def (fun n => 1 + ε n) Nat.cast]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n ↦ 1 + ε n) ∘ Nat.cast) atTop (𝓝 1)
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.inter M2).acceptsFrom (s1, s2) = M1.acceptsFrom s1 ⊓ M2.acceptsFrom s2

Tactic:
by
  ext x
  simp only [acceptsFrom, Language.mem_inf]
  simp_rw [↑Set.mem_ofPred]
  induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, inter_step, ih]

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

Goal state before:
pp: m n : ℕ
⊢ m < n.size ↔ 2 ^ m ≤ n

Tactic:
rw [← Nat.not_lt, Decidable.iff_not_comm, Nat.not_lt, size_le]

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

Goal state before:
pp: m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + ↑m + 1 ≤ ↑n + ↑n

Tactic:
add_assoc

Goal state after:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
h : m.toZNum = n.toZNum
⊢ m = n

Tactic:
cases m <;> cases n <;> cases h <;> rfl

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ FRespects f₂ tr a₂ none ↔ FRespects f₂ tr b₂ none

Tactic:
unfold FRespects

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₂ a₂ = none) ↔
    match none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case mk
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
d : Dir
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move d { head := head✝, left := left✝, right := right✝ }) =
    move d (map f { head := head✝, left := left✝, right := right✝ })

Tactic:
cases d

Goal state after:
case mk.left
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move Dir.left { head := head✝, left := left✝, right := right✝ }) =
    move Dir.left (map f { head := head✝, left := left✝, right := right✝ })

case mk.right
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move Dir.right { head := head✝, left := left✝, right := right✝ }) =
    move Dir.right (map f { head := head✝, left := left✝, right := right✝ })
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact
          ⟨disjoin_manyOneReducible (hl₁.trans OneOneReducible.disjoin_left.to_many_one)
              (hl₂.trans OneOneReducible.disjoin_right.to_many_one),
            disjoin_manyOneReducible (hr₁.trans OneOneReducible.disjoin_left.to_many_one)
              (hr₂.trans OneOneReducible.disjoin_right.to_many_one)⟩

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

Goal state before:
pp: case some.move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
d : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))

Tactic:
cases d

Goal state after:
case some.move.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move Dir.left q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.left q) v (Tape.mk' L R)))

case some.move.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move Dir.right q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.right q) v (Tape.mk' L R)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.write (f (ListBlank.cons a R).head v) q)) v (trTape' enc0 L (ListBlank.cons a R)))
    (trCfg enc enc0
      (stepAux q v (Tape.write (f (Tape.mk' L (ListBlank.cons a R)).head v) (Tape.mk' L (ListBlank.cons a R)))))

Tactic:
tr,

Goal state after:
case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (write (enc (f (ListBlank.cons a R).head v)).toList (move n Dir.left (trNormal dec q))) v
      (trTape' enc0 L (ListBlank.cons a R)))
    (trCfg enc enc0
      (stepAux q v (Tape.write (f (Tape.mk' L (ListBlank.cons a R)).head v) (Tape.mk' L (ListBlank.cons a R)))))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : 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
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ 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.move d q))

Tactic:
cases d

Goal state after:
case move.left
Γ : 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
q : Stmt Γ Λ σ
hw : ∀ 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')
hs : SupportsStmt S (Stmt.move Dir.left q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.left q))

case move.right
Γ : 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
q : Stmt Γ Λ σ
hw : ∀ 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')
hs : SupportsStmt S (Stmt.move Dir.right q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.right q))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i

Tactic:
split_ifs <;> rw [Function.update_of_ne h', ← proj_map_nth, hL]

Goal state after:
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = (S k).length
⊢ (ListBlank.mk (List.map some (S k')).reverse).nth i =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg
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
k' : K
i : ℕ
h' : ¬k' = k
⊢ (if i = tl.length then update (L.nth i) k none else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i

Tactic:
split_ifs <;> rw [Function.update_of_ne h', ← proj_map_nth, hL]

Goal state after:
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
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = tl.length
⊢ (ListBlank.mk (List.map some (S k')).reverse).nth i =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i
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:
have : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesLimit _ (compHausLikeToTop _))

Goal state after:
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
this : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P')
⊢ PreservesLimit (cospan f g) (toCompHausLike h)
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) }
⊢ TM1.stepAux (tr M (ret q)) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
tr,

Goal state after:
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) }
⊢ TM1.stepAux (branch (fun a x ↦ a.1) (trNormal q) (move Dir.left (goto fun x x_1 ↦ ret q))) v
      ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: a b : Λ'
⊢ Decidable (a = b)

Tactic:
by
  induction a generalizing b <;> cases b
  case move.move p k₁ k₂ q _ p' k₁' k₂' q' =>
    exact decidable_of_iff' (p = p' ∧ k₁ = k₁' ∧ k₂ = k₂' ∧ q = q') (by simp)
  case clear.clear p k q _ p' k' q' => exact decidable_of_iff' (p = p' ∧ k = k' ∧ q = q') (by simp)
  case copy.copy q _ q' => exact decidable_of_iff' (q = q') (by simp)
  case push.push k s q _ k' s' q' => exact decidable_of_iff' (k = k' ∧ s = s' ∧ q = q') (by simp)
  case read.read f _ f' => exact decidable_of_iff' (∀ a, f a = f' a) (by simp [funext_iff])
  case succ.succ q _ q' => exact decidable_of_iff' (q = q') (by simp)
  case pred.pred q₁ q₂ _ _ q₁' q₂' => exact decidable_of_iff' (q₁ = q₁' ∧ q₂ = q₂') (by simp)
  case ret.ret k k' => exact decidable_of_iff' (k = k') (by simp)
  all_goals exact .isFalse (by rintro ⟨⟨⟩⟩)

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨V : Set s, VisClopen, Vx, V_sub⟩ := compact_exists_isClopen_in_isOpen u_open_in_s xs

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝³ : TopologicalSpace A
inst✝² : ExtremallyDisconnected A
inst✝¹ : CompactSpace A
inst✝ : T2Space A
B : Type u
⊢ ∀ {Z : Type u} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace Z] [CompactSpace B] [T2Space B] [CompactSpace Z]
    [T2Space Z] {f : A → Z} {g : B → Z}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
C

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_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
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
⊢ closure s = univ

Tactic:
cases preconnectedSpace_iff_clopen.mp h' (closure s) ⟨isClosed_closure, h.open_closure s hs⟩

Goal state after:
case inl
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h✝ : closure s = ∅
⊢ closure s = univ

case inr
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h✝ : closure s = univ
⊢ closure s = univ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B : CompHaus
⊢ ∀ {X_1 : CompHaus} (f : toCompHaus.obj X ⟶ X_1) (e : B ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
C

Goal state after:
X : Stonean
B C : CompHaus
⊢ ∀ (f : toCompHaus.obj X ⟶ C) (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
⊢ ∃ f', f' ≫ f = φ

Tactic:
have : ExtremallyDisconnected (toCompHaus.obj X).toTop := X.prop

Goal state after:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toCompHaus.obj X).toTop
⊢ ∃ f', f' ≫ f = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B : Profinite
⊢ ∀ {X_1 : Profinite} (f : toProfinite.obj X ⟶ X_1) (e : B ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
C

Goal state after:
X : Stonean
B C : Profinite
⊢ ∀ (f : toProfinite.obj X ⟶ C) (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X B : Stonean
⊢ ∀ {X_1 : Stonean} (f : X ⟶ X_1) (e : B ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
C

Goal state after:
X B C : Stonean
⊢ ∀ (f : X ⟶ C) (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = f
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ a, d.proj ⁻¹' {a} = x✝) → ∃ y, x✝ = {x | d.toSetoid x y}

Tactic:
refine fun ⟨y, h⟩ ↦ ⟨Quotient.out (s := d.toSetoid) y, ?_⟩

Goal state after:
case mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ a, d.proj ⁻¹' {a} = x✝¹
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝¹
⊢ x✝¹ = {x | d.toSetoid x y.out}
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ a, d.proj ⁻¹' {a} = x✝²
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝²
x✝ : X
⊢ x✝ ∈ x✝² ↔ x✝ ∈ {x | d.toSetoid x y.out}

Tactic:
simpa [← h] using! Quotient.mk_eq_iff_out (s := d.toSetoid)

Goal state after: