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

Goal state before:
pp: case intro.refine_1
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val✝ : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ Disjoint M.support M'.support

pp: case intro.refine_2
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val✝ : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ (M ⊔ M').IsSpanning

Tactic:
· simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]

Goal state after:
case intro.refine_2
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val✝ : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ (M ⊔ M').IsSpanning
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) 0 = (unpair p).1 - 0

Tactic:
simp [*, Nat.sub_add_eq]

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

Goal state before:
pp: case succ
p n✝ : ℕ
a✝ : Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) n✝ = (unpair p).1 - n✝
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) (n✝ + 1) = (unpair p).1 - (n✝ + 1)

Tactic:
simp [*, Nat.sub_add_eq]

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

Goal state before:
pp: α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode (decode n) = encode (Option.map (⇑e.symm) (decode n))

Tactic:
cases (@decode α _ n)

Goal state after:
case none
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode none = encode (Option.map (⇑e.symm) none)

case some
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map (⇑e.symm) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
c : α → Prop
inst✝ : DecidablePred c
f g : α → σ
hc : PrimrecPred c
hf : Primrec f
hg : Primrec g
⊢ Primrec fun a ↦ if c a then f a else g a

Tactic:
simpa [Bool.cond_decide] using cond hc.decide hf hg

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
⊢ Primrec fun a ↦ some (f a)

Tactic:
have := decidableEqOfEncodable α

Goal state after:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
⊢ Primrec fun a ↦ some (f a)
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₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
⊢ ((↑(decode n)).bind fun a ↦
      map encode
        ((fun a ↦
            (do
                  let n ← (↑fun n ↦ encode (decode n)) a.2
                  ↑n.ppred).bind
              ↑fun b ↦ (fun a n ↦ (decode n).bind (f a)) (a, b).1.1 (a, b).1.2)
          a)) =
    (↑(decode n)).bind fun a ↦ map encode ((↑fun p ↦ f p.1 p.2) a)

Tactic:
simp only [decode_prod_val, decode_nat, Option.map_some, PFun.coe_val, bind_eq_bind,
          bind_some, Part.map_bind, map_some]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
⊢ ((↑((decode (Nat.unpair n).1).bind fun a ↦ Option.some (a, (Nat.unpair n).2))).bind fun a ↦
      (↑(encode (decode a.2)).ppred).bind fun y ↦ Part.some (encode ((decode a.2).bind fun a_1 ↦ f a.1 a_1))) =
    (↑((decode (Nat.unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a ↦
      Part.some (encode (f a.1 a.2))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : 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]?
⊢ Primrec f

Tactic:
exact option_some_iff.mp <| this.of_eq <| fun b ↦ by
    have graph_eq_map_bindList (i : ℕ) (hi : i ≤ m b + 1) :
        graph b i = (bindList b (m b + 1 - i)).map fun x ↦ (x, f x) := by
      have bindList_eq_nil : bindList b (m b + 1) = [] :=
        have bindList_m_lt (k : ℕ) : ∀ b' ∈ bindList b k, m b' < m b + 1 - k := by
          induction k with simp [bindList]
          | succ k ih =>
            grind
        List.eq_nil_iff_forall_not_mem.mpr
          (by intro b' ha'; by_contra; simpa using bindList_m_lt (m b + 1) b' ha')
      have mapGraph_graph {bs bs' : List β} (has : bs' ⊆ bs) :
          mapGraph (bs.map <| fun x => (x, f x)) bs' = bs'.map f := by
        induction bs' with simp [mapGraph]
        | cons b bs' ih =>
          have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has
          rcases this with ⟨ha, has'⟩
          simpa [List.lookup_graph f ha] using ih has'
      have graph_succ : ∀ i, graph b (i + 1) =
        (bindList b (m b - i)).filterMap fun b' =>
          (g b' <| mapGraph (graph b i) (l b')).map (b', ·) := fun _ => rfl
      have bindList_succ : ∀ i, bindList b (i + 1) = (bindList b i).flatMap l := fun _ => rfl
      induction i with
      | zero => symm; simpa [graph] using bindList_eq_nil
      | succ i ih =>
        simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.le_of_lt_succ hi),
          Nat.succ_eq_add_one, bindList_succ, Nat.reduceSubDiff]
        apply List.filterMap_eq_map_iff_forall_eq_some.mpr
        intro b' ha'; simp; rw [mapGraph_graph]
        · exact H b'
        · exact (List.infix_flatMap_of_mem ha' l).subset
    simp [graph_eq_map_bindList (m b + 1) (Nat.le_refl _), bindList]

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

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ IH - 1) 0 = v.tail.head - 0

Tactic:
simp [*, Nat.sub_add_eq]

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

Goal state before:
pp: case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec v.tail.head (fun y IH ↦ IH - 1) n✝ = v.tail.head - n✝
⊢ Nat.rec v.tail.head (fun y IH ↦ IH - 1) (n✝ + 1) = v.tail.head - (n✝ + 1)

Tactic:
simp [*, Nat.sub_add_eq]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
⊢ (∃ M, M.IsPerfectMatching) → ∀ (u : Set V), ¬G.IsTutteViolator u

Tactic:
rintro ⟨M, hM⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
⊢ ∀ (u : Set V), ¬G.IsTutteViolator u
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially 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, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
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|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |f u| * |g u| ≤ c₂ * |f x| * (c₄ * |g x|)

Tactic:
by
           gcongr
           · exact (hf u hu).2
           · exact (hg u hu).2

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : ℕ →. ℕ
⊢ Nat.Partrec f ↔ ∃ c, c.eval = f

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
  · rintro ⟨c, rfl⟩
    induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm

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

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

Tactic:
induction n using binaryRec' with

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.none.bind fun a ↦ evaln k c a) = evaln k c n

Tactic:
cases e : evaln k c n

Goal state after:
case neg.none
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
e : evaln k c n = Option.none
⊢ (Option.none.bind fun a ↦ evaln k c a) = Option.none

case neg.some
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
val✝ : ℕ
e : evaln k c n = some val✝
⊢ (Option.none.bind fun a ↦ evaln k c a) = some val✝
Module: Mathlib.Data.Num.Bitwise

Goal state before:
pp: C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (nz (msb b))

Tactic:
← bit_one

Goal state after:
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (b::zero (decide ¬b = true))
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts

Tactic:
by
  simp [mem_accepts, ← Set.not_disjoint_iff, disjoint_evalFrom_reverse_iff]

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
v : List.Vector ℕ n
⊢ (mOfFn fun i ↦ Fin.cases f (fun i v ↦ ↑(some (v.get i))) i v) >>= g = (f v).bind fun a ↦ g (a ::ᵥ v)

Tactic:
simp [mOfFn, Part.bind_assoc, pure]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
⊢ Reaches₁ f₂ b✝ g₂ → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
cg

Goal state after:
case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ b✝ g₂
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
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)

Tactic:
change (R.cons a).nth (n + 1) = R.nth n

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (ListBlank.cons a R).nth (n + 1) = R.nth n
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some
Γ : 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 : σ
q : TM1.Stmt Γ Λ σ
q' : Option (TM1.Stmt Γ Λ σ)
v' : σ
h₁ : ((q', v'), s) ∈ tr M (some q, v) a
h₂ : some q ∈ TM1.stmts M S
⊢ q' ∈ TM1.stmts M S

Tactic:
cases q'

Goal state after:
case right.some.none
Γ : 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 : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
h₁ : ((none, v'), s) ∈ tr M (some q, v) a
⊢ none ∈ TM1.stmts M S

case right.some.some
Γ : 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 : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : ((some val✝, v'), s) ∈ tr M (some q, v) a
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: 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))
i : ℕ
h : i = (S k).length
⊢ some (f v) = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

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))
i : ℕ
h : ¬i = (S k).length
⊢ L.nth i k = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
· rw [List.getI_eq_getElem _, List.getElem_append_right] <;>
        simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]

Goal state after:
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))
i : ℕ
h : ¬i = (S k).length
⊢ L.nth i k = ((List.map some (S k)).reverse ++ [some (f v)]).getI i
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option.refine_1
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'
⊢ ∀ (i : Option I), IsClopen (C i)

Tactic:
rintro (_ | i); all_goals grind

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

Goal state before:
pp: case h_option.refine_2
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'
⊢ ∀ (i : Option I), Z i ⊆ C i

Tactic:
rintro (_ | i); all_goals grind

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

Goal state before:
pp: case h_option.refine_3
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'
⊢ ∀ (i : Option I), C i ⊆ D i

Tactic:
rintro (_ | i); all_goals grind

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

Goal state before:
pp: case h_option.refine_4
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'
⊢ ⋃ i, D i ⊆ ⋃ i, C i

Tactic:
rintro (_ | i); all_goals grind

Goal state after: