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

Goal state before:
pp: case neg.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 : 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
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x x' ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
·

Goal state after:
case neg.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 : 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
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x x' ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
⊢ (Nat.casesOn (encode Option.none) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn Option.none (Part.some (f a)) (g a)

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
b : β
⊢ (Nat.casesOn (encode (Option.some b)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn (Option.some b) (Part.some (f a)) (g a)

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_1
α : 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 : ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
⊢ b ∈ f.fix a

pp: case 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
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n

Tactic:
·

Goal state after:
case refine_1
α : 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 : ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
⊢ b ∈ f.fix a
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: R : ℕ → ℕ → Prop
s : ℕ
inst✝ : DecidableRel R
hf : PrimrecRel R
⊢ Primrec₂ fun n ↦ Option.guard fun y ↦ decide (R y n)

Tactic:
refine ite (Primrec.eq.comp ?_ (const true)) (option_some_iff.mpr snd) (.const Option.none)

Goal state after:
R : ℕ → ℕ → Prop
s : ℕ
inst✝ : DecidableRel R
hf : PrimrecRel R
⊢ Primrec fun p ↦ (fun y ↦ decide (R y p.1)) p.2
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ PrimrecPred fun p ↦ (fun a ↦ decide (R a p.1.2)) p.2 = true

pp: case refine_2
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec fun p ↦ some p.2

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ PrimrecPred fun p ↦ (fun a ↦ decide (R a p.1.2)) p.2 = true
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec fun p ↦ some p.2

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec fun p ↦ some p.2
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case 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
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n

Tactic:
·

Goal state after:
case 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
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
e : b v - a v = 0
⊢ Nat.rec (g v) (fun y IH ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) 0 = if a v < b v then f v else g v

pp: case succ
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
n✝ : ℕ
e : b v - a v = n✝ + 1
⊢ Nat.rec (g v) (fun y IH ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (n✝ + 1) = if a v < b v then f v else g v

Tactic:
·

Goal state after:
case zero
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
e : b v - a v = 0
⊢ Nat.rec (g v) (fun y IH ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) 0 = if a v < b v then f v else g v
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
n✝ : ℕ
e : b v - a v = n✝ + 1
⊢ Nat.rec (g v) (fun y IH ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (n✝ + 1) = if a v < b v then f v else g v

Tactic:
·

Goal state after:
case succ
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
n✝ : ℕ
e : b v - a v = n✝ + 1
⊢ Nat.rec (g v) (fun y IH ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (n✝ + 1) = if a v < b v then f v else g v
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case refine_2
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
this :
  Primrec' fun v ↦
    Nat.rec 0
      (fun y IH ↦
        have x := (y ::ᵥ IH ::ᵥ v).head;
        have y := (y ::ᵥ IH ::ᵥ v).tail.head;
        if x.succ < y.succ * y.succ then y else y.succ)
      v.head
⊢ Primrec' fun v ↦ Nat.rec 0 (fun x y ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head

pp: case refine_1
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
⊢ Primrec' fun v ↦
    have x := v.head;
    have y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ

Tactic:
·

Goal state after:
case refine_2
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
this :
  Primrec' fun v ↦
    Nat.rec 0
      (fun y IH ↦
        have x := (y ::ᵥ IH ::ᵥ v).head;
        have y := (y ::ᵥ IH ::ᵥ v).tail.head;
        if x.succ < y.succ * y.succ then y else y.succ)
      v.head
⊢ Primrec' fun v ↦ Nat.rec 0 (fun x y ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head
Module: Mathlib.Computability.Primrec.List

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

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case refine_2.inl
α : 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₂
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

pp: case refine_2.inr
α : 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
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
·

Goal state after:
case refine_2.inl
α : 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₂
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2.inl.refine_1
α : 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₂
⊢ Sum.inl b ∈ F a k.succ

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 m

Tactic:
·

Goal state after:
case refine_2.inl.refine_1
α : 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₂
⊢ Sum.inl b ∈ F a k.succ
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 m

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 m
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
this : ∀ (f : ℕ → ℕ), Nat.Primrec f → Primrec' fun v ↦ f v.head
hf : Primrec f
i : List.Vector ℕ n
⊢ (encode (Option.map f (decode (encode i)))).pred = f i

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2.inr
α : 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
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
·

Goal state after:
case refine_2.inr
α : 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
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
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:
apply ack_strictMono_right _ (ack_strictMono_right _ _)

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

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

Tactic:
by lia

Goal state after:
Module: Mathlib.Computability.Ackermann

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

Tactic:
by lia

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case zero
m : ℕ
⊢ ack m (0 + 1) ≤ ack (m + 1) 0

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

Tactic:
·

Goal state after:
case zero
m : ℕ
⊢ ack m (0 + 1) ≤ ack (m + 1) 0
Module: Mathlib.Computability.Ackermann

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

Tactic:
·

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

Goal state before:
pp: m n : ℕ
⊢ m ≤ m + 2

Tactic:
by lia

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

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n

Tactic:
obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_le hb
  exact ⟨c, hc_mem, hc.natCast_atTop⟩

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

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u

Tactic:
obtain ⟨c₁, hc₁, c₂, _, h⟩ := hf b hb
  refine ⟨c₁, hc₁, ?_⟩
  filter_upwards [h]
  exact fun _ H u hu => (H u hu).1

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: 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))

pp: 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))

Tactic:
·

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))
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inr.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 ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : ?m.418 < n
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + (n + 1))

pp: case inr.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 ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ ?m.418
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
·

Goal state after:
case inr.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 ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : ?m.418 < n
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + (n + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∃ K, ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
·

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∃ K, ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
·

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∃ K, ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: h : Nat.Primrec fun n ↦ ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False

Tactic:
exact (hm m).false

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case hf
⊢ Partrec fun p ↦ (pappAck p.1).eval p.2

pp: case H
⊢ ∀ (n : ℕ × ℕ), ack n.1 n.2 ∈ (pappAck n.1).eval n.2

Tactic:
·

Goal state after:
case hf
⊢ Partrec fun p ↦ (pappAck p.1).eval p.2