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

Goal state before:
pp: case refine_1.hsu.inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this✝ : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x', b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ x' ≠ a

pp: case refine_1.hsu.inr
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this✝ : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, x'}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ x' ≠ a

Tactic:
exacts [hxa.ne, hab.ne.symm]

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

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
⊢ Nat.rec (some [])
      (fun n IH ↦
        (a, n, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      n =
    some (List.map (f a) (List.range n))

Tactic:
induction n with
      | zero => rfl
      | succ n IH => simp [IH, H, List.range_succ]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p m

Tactic:
]

Goal state after:
case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p m
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ m ∈ rfind p

Tactic:
]

Goal state after:
case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ m ∈ rfind p
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ n ∈ rfind p

Tactic:
rwa [← h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
hx' : x' ∈ {x, b}
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
⊢ p.toSubgraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
hx' : x' ∈ {x, b}
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
⊢ p.toSubgraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x', b}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x' c'

Tactic:
]

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x', b}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x' c'
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x, x'}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj c' x'

Tactic:
]

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x, x'}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj c' x'
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : ℕ → ℕ →. α
h : Partrec (Nat.unpaired f)
⊢ Partrec₂ f

Tactic:
simpa using! Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
x✝ : ℕ × List α
n : ℕ
l : List α
⊢ (List.drop ((n, l).2.length - (n, l).1) (n, l).2.reverse).reverse = (List.drop (l.length - n) l.reverse).reverse

Tactic:
]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
a' : α
ba : b ∈ f.fix a'
am : a' = a
⊢ b ∈ f.fix a'

Tactic:
]

Goal state after:
case zero
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
a' : α
ba : b ∈ f.fix a'
am : a' = a
⊢ b ∈ f.fix a'
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i ↦ v.get i.succ) = f (ofFn v.tail.get)

Tactic:
]

Goal state after:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i ↦ v.get i.succ) = f (ofFn v.tail.get)
Module: Mathlib.Computability.Primrec.List

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

Tactic:
]

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

Goal state before:
pp: v : List.Vector ℕ 0
⊢ 0 = encode nil

Tactic:
]

Goal state after:
v : List.Vector ℕ 0
⊢ 0 = encode nil
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
n : ℕ
IH : Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt

Tactic:
]

Goal state after:
case succ
n : ℕ
IH : Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
| n + 4

Tactic:
← Nat.bit_bodd_div2 n,

Goal state after:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
| bit n.bodd n.div2 + 4
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case prec
n : ℕ
f✝¹ : List.Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
hf : Primrec' fun v ↦ f✝ v.head
hg : Primrec' fun v ↦ g✝ v.head
⊢ Primrec' fun v ↦ unpaired (fun z n ↦ Nat.rec (f✝ z) (fun y IH ↦ g✝ (pair z (pair y IH))) n) v.head

Tactic:
simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2.inl.refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂✝ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
m : ℕ
mk : m < k.succ
km : k ≤ m
⊢ Sum.inr a₂ ∈ F a k

Tactic:
]

Goal state after:
case refine_2.inl.refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂✝ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
m : ℕ
mk : m < k.succ
km : k ≤ m
⊢ Sum.inr a₂ ∈ F a k
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ n + 1 = n + 1

Tactic:
]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ ack m 1 = ack m 1

Tactic:
]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ ack m (ack (m + 1) n) = ack m (ack (m + 1) n)

Tactic:
]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 3 (n + 1) = 2 ^ (n + 1 + 3) - 3

Tactic:
ack_succ_succ,

Goal state after:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 2 (ack (2 + 1) n) = 2 ^ (n + 1 + 3) - 3
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 2 ^ (n + 3) - 3 = 2 * 2 ^ (n + 3) - 3

pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
]

Goal state after:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ 0 < ack m 1

Tactic:
]

Goal state after:
m : ℕ
⊢ 0 < ack m 1
Module: Mathlib.Computability.Ackermann

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
m : ℕ
⊢ 1 < ack (m + 1) 1
Module: Mathlib.Computability.Ackermann

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

Tactic:
]

Goal state after:
m n : ℕ
⊢ 1 < ack (m + 1) (ack (m + 1 + 1) n)
Module: Mathlib.Computability.Ackermann

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

Tactic:
]

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

Goal state before:
pp: m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)

Tactic:
ack_succ_succ,

Goal state after:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack (m + 1) (n₂ + 1)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)

Tactic:
]

Goal state after:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n₁ n₂ : ℕ
h : n₁ < n₂
⊢ n₁ < n₂

Tactic:
]

Goal state after:
m n₁ n₂ : ℕ
h : n₁ < n₂
⊢ n₁ < n₂
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ m + n + 2 = m + 1 + n + 1

Tactic:
]

Goal state after:
m n : ℕ
⊢ m + n + 2 = m + 1 + n + 1
Module: Mathlib.Computability.Ackermann

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

Tactic:
]

Goal state after:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)

Tactic:
ack_succ_succ,

Goal state after:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack (m₂ + 1) (n + 1)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)

Tactic:
]

Goal state after:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)

Tactic:
]

Goal state after:
case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
]

Goal state after:
cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1

Tactic:
]

Goal state after:
m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ (ack (m + 1) (n + 1) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)

Tactic:
ack_succ_succ,

Goal state after:
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)

Tactic:
]

Goal state after:
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
Module: Mathlib.Computability.Ackermann

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

Tactic:
]

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

Goal state before:
pp: case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).1) n ≤ n

Tactic:
]

Goal state after:
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).1) n ≤ n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
⊢ encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)

Tactic:
have : encode (pair cf cg) < encode (prec cf cg) := by simp [encodeCode_eq, encodeCode]

Goal state after:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.prec cg)
⊢ encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).2) n ≤ n

Tactic:
]

Goal state after:
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).2) n ≤ n
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
n : ℕ
⊢ (max (f n) (g n) + 1) ^ 2 ≤ (max (ack a n) (ack b n) + 1) ^ 2

Tactic:
]

Goal state after:
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
n : ℕ
⊢ (max (f n) (g n) + 1) ^ 2 ≤ (max (ack a n) (ack b n) + 1) ^ 2