mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inr
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
hx : x ∈ ↑s
⊢ False

Tactic:
| inr hx =>

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
x : α
hx : x ∈ Xᶜ
⊢ ∃ y ∈ s ∩ t, ¬G.Adj x y

Tactic:
contrapose! hx

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
x : α
hx : ∀ y ∈ s ∩ t, G.Adj x y
⊢ x ∉ Xᶜ
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c d : Set V
hcd : c ⊆ d
hc : G.IsVertexCover c
⊢ G.IsVertexCover d

Tactic:
by
  grind [IsVertexCover]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α := ⋯
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
l : List α
n : ℕ
⊢ l[n]? = Sum.rec (fun val ↦ none) (fun val ↦ some val) (F l n)

Tactic:
induction l generalizing n with

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
d : α
⊢ Primrec₂ fun l n ↦ l.getD n d

Tactic:
by
  simp only [List.getD_eq_getElem?_getD]
  exact option_getD.comp₂ list_getElem? (const _)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
⊢ Computable₂ fun a n ↦ (decode n).bind (f a)

Tactic:
have :
      Partrec fun a : α × ℕ =>
        (encode (decode (α := β) a.2)).casesOn (some Option.none)
          fun n => Part.map (f a.1) (decode (α := β) n) :=
      Partrec.nat_casesOn_right
        (h := fun (a : α × ℕ) (n : ℕ) ↦ map (fun b ↦ f a.1 b) (Part.ofOption (decode n)))
        (Primrec.encdec.to_comp.comp snd) (const Option.none)
        ((ofOption (Computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a ↦ Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)
⊢ Computable₂ fun a n ↦ (decode n).bind (f a)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 0).encodeCode = 0

Tactic:
simp [ofNatCode, encodeCode]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 1).encodeCode = 1

Tactic:
simp [ofNatCode, encodeCode]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 2).encodeCode = 2

Tactic:
simp [ofNatCode, encodeCode]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 3).encodeCode = 3

Tactic:
simp [ofNatCode, encodeCode]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
f : ℕ → ℕ
n : ℕ
⊢ n.succ < ack 1 n

Tactic:
succ_eq_one_add

Goal state after:
case succ
f : ℕ → ℕ
n : ℕ
⊢ 1 + n < ack 1 n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: c : ℝ
hc : c < 1
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Tactic:
have h₁ : Tendsto (fun x => 1 - ε x) atTop (𝓝 1) := by
    rw [← isEquivalent_const_iff_tendsto one_ne_zero]
    exact isEquivalent_one_sub_smoothingFn_one
  rw [tendsto_order] at h₁
  exact h₁.1 c hc

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case h
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
    (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁

Goal state after:
case right
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
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
⊢ asympBound g a b =O[atTop] T

Tactic:
calc asympBound g a b
    _ = (fun n => 1 * asympBound g a b n) := by simp
    _ ~[atTop] (fun n => (1 + ε n) * asympBound g a b n) := by
      refine IsEquivalent.mul (IsEquivalent.symm ?_) IsEquivalent.refl
      rw [Function.const_def, isEquivalent_const_iff_tendsto one_ne_zero,
        ← Function.comp_def (fun n => 1 + ε n) Nat.cast]
      exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const
        tendsto_natCast_atTop_atTop
    _ =O[atTop] T := R.smoothingFn_mul_asympBound_isBigO_T

Goal state after:
Module: Mathlib.Computability.DFA

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

Tactic:
simp only [acceptsFrom, Language.mem_inf]

Goal state after:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ x ∈ {x | (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept} ↔
    x ∈ {x | M1.evalFrom s1 x ∈ M1.accept} ∧ x ∈ {x | M2.evalFrom s2 x ∈ M2.accept}
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case ub
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_pos : 0 < f x
hf_pos₂ : ∀ (y : ℝ), b * id x ≤ y → 0 < f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ^ p ≤ c₁ ^ p * f x ^ p

Tactic:
case ub => calc
        (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.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p + ↑↑p = ↑p + ↑p

Tactic:
p.cast_to_nat

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑p + ↑p = ↑p + ↑p
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p + ↑↑p + 1 = ↑p + ↑p + 1

Tactic:
p.cast_to_nat

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑p + ↑p + 1 = ↑p + ↑p + 1
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x

Tactic:
induction x generalizing S T with
  | nil => simp
  | cons a x ih => simp [ih]

Goal state after:
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:
ofNat'_bit true n,

Goal state after:
case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif true then Num.bit1 else Num.bit0) (ofNat' n) = ofNat' (Nat.bit false n) + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case succ
m n✝ : ℕ
a✝ : ofNat' (m + n✝) = ofNat' m + ofNat' n✝
⊢ ofNat' (m + (n✝ + 1)) = ofNat' m + ofNat' (n✝ + 1)

Tactic:
· simp only [Nat.add_succ, Nat.add_zero, ofNat'_succ, add_one, add_succ, *]

Goal state after:
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', x'.reduceOption = x.concat a ∧ M.IsPath s₁ s₂ x') →
    ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
List.reduceOption_eq_concat_iff,

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', (∃ l₁ l₂, x' = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = x ∧ l₂.reduceOption = []) ∧ M.IsPath s₁ s₂ x') →
    ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖

Tactic:
simp [c₁_cancel]; ring

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).head = f.f l.head

Tactic:
by
  rw [← ListBlank.cons_head_tail l]
  induction l using Quotient.inductionOn'
  rfl

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).tail = map f l.tail

Tactic:
by
  rw [← ListBlank.cons_head_tail l]
  induction l using Quotient.inductionOn'
  rfl

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
O O' : Set (ℕ →. ℕ)
f : α →. σ
hf : RecursiveIn O f
hO : ∀ g ∈ O, RecursiveIn O' g
⊢ ∀ g ∈ O, Nat.RecursiveIn O' g

Tactic:
by simpa only [RecursiveIn.iff_nat] using hO

Goal state after:
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
rcases x with - | ⟨a, x⟩
      · intro _h
        use []; dsimp; tauto
      · rw [rmatch, deriv, mul_rmatch_iff]
        rintro ⟨t, u, hs, ht, hu⟩
        have hwf : u.length < (List.cons a x).length := by
          rw [hs, List.length_cons, List.length_append]
          lia
        rw [IH _ hwf] at hu
        rcases hu with ⟨S', hsum, helem⟩
        use (a :: t) :: S'
        constructor
        · simp [hs, hsum]
        · intro t' ht'
          cases ht' with
          | head ht' =>
            simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
            exact ht
          | tail _ ht' => exact helem t' ht'

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

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

Tactic:
addBottom_nth_snd,

Goal state after:
case right.e_a.e_a.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ L.nth tail✝.length k = (head✝ :: tail✝).head?
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
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
⊢ TM1.stepAux q (f v (((addBottom L).nth tl.length).2 k))
      ((Tape.move Dir.right)^[tl.length]
        (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L)))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))

Tactic:
addBottom_nth_snd,

Goal state after:
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
⊢ TM1.stepAux q (f v (L.nth tl.length k))
      ((Tape.move Dir.right)^[tl.length]
        (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L)))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))
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 Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ 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) }

Tactic:
by
  induction n with
  | zero => rfl
  | succ n IH =>
    refine Reaches₀.head ?_ IH
    simp only [Option.mem_def, TM1.step]
    rw [Option.some_inj, tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat,
      addBottom_nth_succ_fst, TM1.stepAux, iterate_succ', Function.comp_apply, Tape.move_right_left]
    rfl

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

Goal state before:
pp: case mp
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
suffices ∀ c, x ∈ eval step c → ∀ v c', c = Cfg.then c' (Cont.fix f k) →
      Reaches step (stepNormal f Cont.halt v) c' →
        ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if List.headI v₁ = 0 then pure v₁.tail else f.fix.eval v₁.tail,
          x ∈ eval step (Cfg.ret k v₂) by
      intro h
      obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
        this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl
      refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
      simp only [Part.eq_some_iff.2 hv₁, Part.map_some]
      split_ifs at hv₂ ⊢
      · rw [Part.mem_some_iff.1 hv₂]
        exact Or.inl (Part.mem_some _)
      · exact Or.inr ⟨_, Part.mem_some _, hv₂⟩

Goal state after:
case mp
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
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)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : ¬v₁.headI = 0
hv₂ : v₂ ∈ f.fix.eval v₁.tail
⊢ False ∨
    ∃ a',
      Sum.inr a' = Sum.inr v₁.tail ∧
        v₂ ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'

Tactic:
exact Or.inr ⟨_, rfl, hv₂⟩

Goal state after:
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
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ y ∈ (closure U)ᶜ

Tactic:
rw [Set.mem_compl_iff, mem_closure_iff]

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
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case none
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.move (fun x ↦ false) rev k₂ q), var := none,
      stk := update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) }
    { l := some q, var := none, stk := update (update S k₁ L₂) k₂ (L₁ ++ S k₂) }

Tactic:
convert! move_ok h₁.2.1.symm (splitAtPred_false _) using 2
    simp only [Function.update_comm h₁.1, Function.update_idem]
    rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]
    simp only [Function.update_of_ne h₁.2.2.symm, Function.update_of_ne h₁.2.1,
      Function.update_of_ne h₁.1.symm, List.reverseAux_eq, h₂, Function.update_self,
      List.append_nil, List.reverse_reverse]

Goal state after:
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
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
have X₁_cont : Continuous X₁ := continuous_fst.comp continuous_subtype_val

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
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ 1 = if f.hom.hom' x ∈ V then 0 else 1

Tactic:
rw [if_neg]

Goal state after:
case hnc
X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ f.hom.hom' x ∉ V