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

Goal state before:
pp: α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert b (insert a (s.erase c)))

Tactic:
← erase_insert_of_ne (fun h : a = c ↦ ha (h ▸ hc) |>.elim)

Goal state after:
α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert b ((insert a s).erase c))
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
⊢ ∃ M, M.IsPerfectMatching

Tactic:
classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩

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 α := ⋯
W : Finset α := ⋯
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ᶜ
⊢ {z ∈ s ∩ t | ¬G.Adj x z}.Nonempty

Tactic:
obtain ⟨_, hy⟩ : ∃ y ∈ s ∩ t, ¬ G.Adj x y := by
      contrapose! hx
      simpa [X] using 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 : x ∈ Xᶜ
w✝ : α
hy : w✝ ∈ s ∩ t ∧ ¬G.Adj x w✝
⊢ {z ∈ s ∩ t | ¬G.Adj x z}.Nonempty
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun p a ↦ p.1

Tactic:
exact fst.comp fst

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

Goal state before:
pp: case cons
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝¹ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this✝ : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
this : b ∈ bs ∧ bs' ⊆ bs
⊢ (List.lookup b (List.map (fun x ↦ (x, f x)) bs)).toList ++
      List.flatMap (fun x ↦ (List.lookup x (List.map (fun x ↦ (x, f x)) bs)).toList) bs' =
    f b :: List.map f bs'

Tactic:
rcases this with ⟨ha, has'⟩

Goal state after:
case cons
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
ha : b ∈ bs
has' : bs' ⊆ bs
⊢ (List.lookup b (List.map (fun x ↦ (x, f x)) bs)).toList ++
      List.flatMap (fun x ↦ (List.lookup x (List.map (fun x ↦ (x, f x)) bs)).toList) bs' =
    f b :: List.map f bs'
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
_h : 0 < n + 1
⊢ ack (m + 1) 0 < ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_zero, ack_succ_succ]

Goal state after:
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
hg' : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hg'⟩ := hg'

Goal state after:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
rcases lt_or_ge _ m with h₁ | h₁

Goal state after:
case inl
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : ?m.338 < m
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + (n + 1))

case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ ?m.338
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + (n + 1))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:

Tactic:
-logb 2 (x / x₀) ≤ ⌈-logb 2 (x / x₀)⌉₊ := Nat.le_ceil (-logb 2 (x / x₀))
         _ ≤ _ := by rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _

Goal state after:
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
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
h_ge_n₀ : R.n₀ ≤ n
h_n_pos : 0 < n
h_bn : 1 < b' * ↑n
⊢ b i * ↑n ≤ 1 * ↑n

Tactic:
by gcongr; exact le_of_lt <| R.b_lt_one i

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 - ε x) x = (-deriv ε) x

Tactic:
rw [deriv_fun_sub] <;> aesop

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 - ε x) x = -deriv ε x

Tactic:
rw [deriv_fun_sub] <;> aesop

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n) =
    (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)

Tactic:
rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case comp
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x : ℕ
h : ∃ a ∈ cg.eval n, x ∈ cf.eval a
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
| comp cf cg hf hg =>

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

Goal state before:
pp: m n : ℕ
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
by_cases h : (m + n) % 2 = 0
  · simp only [h, mod_two_eq_zero_iff_testBit_zero, testBit_zero, xor_mod_two_eq_one, decide_not,
      Bool.decide_iff_dist, Bool.not_eq_false', beq_iff_eq, decide_eq_decide]
    lia
  · simp only [mod_two_ne_zero] at h
    simp only [h, xor_mod_two_eq_one]
    lia

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ n ^^^ 1 = n - 1

Tactic:
by
  cases n with
  | zero =>
    exact not_odd_zero h |>.elim
  | succ n =>
    simp +instances only [HXor.hXor, instXorOp, xor, bitwise, reduceDiv, bitwise_zero_right]
    grind

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

Goal state before:
pp: b : PosNum
⊢ 1 + b.succ = (1 + b).succ

Tactic:
simp [one_add]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ (fun x_1 ↦ x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)

Tactic:
ext y; simp [append_mem_acceptsFrom M]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
x : Option α
⊢ [x].reduceOption = x.toList

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
constructor <;> · exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

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

Goal state before:
pp: ⊢ ↑↑0 = 0

Tactic:
Nat.cast_zero,

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

Goal state before:
pp: case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ (↑n).pred
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Tactic:
← pred'_to_nat,

Goal state after:
case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑n.pred'
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Tactic:
have : (1 : ℕ) ≤ Nat.pred n := Nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h)
    rw [← pred'_to_nat, e] at this
    exact absurd this (by decide)

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

Goal state before:
pp: case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = (↑n).pred

Tactic:
← pred'_to_nat,

Goal state after:
case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = ↑n.pred'
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case refine_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), (mk l₁).nth i = (mk l₂).nth i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

Tactic:
simp only [ListBlank.nth_mk] at H

Goal state after:
case refine_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ RecursiveIn O f ↔ Nat.RecursiveIn O f

Tactic:
simp [RecursiveIn, Part.map_id']

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth (↑(n + 1) + 1 - 1)

Tactic:
rw [add_sub_cancel_right]

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth ↑(n + 1)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right
Γ : 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
q : Λ' M
a : Γ
q' : Λ' M
⊢ ∀ {s : TM0.Stmt Γ}, (q', s) ∈ tr M q a → q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts M S)

Tactic:
s

Goal state after:
case right
Γ : 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
q : Λ' M
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
⊢ (q', s) ∈ tr M q a → q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts 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 Γ
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (ListBlank.cons L.head R)

Tactic:
by
  obtain ⟨a, L, rfl⟩ := L.exists_cons
  simp only [trTape', ListBlank.cons_flatMap, ListBlank.head_cons, ListBlank.tail_cons]
  suffices ∀ {L' R' l₁ l₂} (_ : List.Vector.toList (enc a) = List.reverseAux l₁ l₂),
      (Tape.move Dir.left)^[l₁.length]
      (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (List.Vector.toList (enc a)) R') by
    simpa only [List.length_reverse, Vector.toList_length] using! this (List.reverse_reverse _).symm
  intro _ _ l₁ l₂ e
  induction l₁ generalizing l₂ with
  | nil => cases e; rfl
  | cons b l₁ IH =>
    simp only [List.length, iterate_succ_apply]
    convert! IH e
    simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]

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

Goal state before:
pp: a b c d a' : List Γ'
x : K'
⊢ update (elim a b c d) main a' x = elim a' b c d x

Tactic:
cases x <;> rfl

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

Goal state before:
pp: a b c d b' : List Γ'
x : K'
⊢ update (elim a b c d) rev b' x = elim a b' c d x

Tactic:
cases x <;> rfl

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

Goal state before:
pp: a b c d c' : List Γ'
x : K'
⊢ update (elim a b c d) aux c' x = elim a b c' d x

Tactic:
cases x <;> rfl

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

Goal state before:
pp: a b c d d' : List Γ'
x : K'
⊢ update (elim a b c d) stack d' x = elim a b c d' x

Tactic:
cases x <;> rfl

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

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

Tactic:
s

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

Goal state before:
pp: case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty

Tactic:
have is_open : IsOpen <| G ∩ ρ ⁻¹' N := hG.inter <| N_open.preimage ρ_cont

Goal state after:
case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
⊢ ρ x₁ = ρ x₂ → x₁ = x₂

Tactic:
hρx

Goal state after:
A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
⊢ x₁ = x₂
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case pos
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
x : X
hx : ∃ i, x ∈ D i
hx0 : x ∈ C0
⊢ ∃ i, x ∈ C i

Tactic:
exact ⟨none, hx0⟩

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
⊢ W = I.sup ((fun i ↦ i.1 ×ˢ i.2) ∘ fun x ↦ (U x, V x))

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)

Goal state after:
case h.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
x : X × Y
hx : x ∈ W
⊢ x ∈ I.sup ((fun i ↦ i.1 ×ˢ i.2) ∘ fun x ↦ (U x, V x))

case h.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
x : X × Y
hx : x ∈ I
⊢ ((fun i ↦ i.1 ×ˢ i.2) ∘ fun x ↦ (U x, V x)) x ≤ W
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: S : LightDiagram
n : ℕ
⊢ Finite ↑((S.diagram ⋙ toProfinite).obj (op n)).toTop

Tactic:
simp only [Functor.comp_obj]

Goal state after:
S : LightDiagram
n : ℕ
⊢ Finite ↑(toProfinite.obj (S.diagram.obj (op n))).toTop