mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn (f a) (g a) fun b ↦ b) = (f a).getD (g a)

Tactic:
cases f a

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn Option.none (g a) fun b ↦ b) = Option.none.getD (g a)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
val✝ : β
⊢ (Option.casesOn (Option.some val✝) (g a) fun b ↦ b) = (Option.some val✝).getD (g a)
Module: Mathlib.Computability.Partrec

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

Tactic:
simp [IH, H, List.range_succ]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a ↦
    Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)
a : α
⊢ (Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (f a) (fun b ↦ Part.some (g a b)) (h a))

Tactic:
cases f a

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a ↦
    Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)
a : α
val✝ : β
⊢ (Option.casesOn (Sum.casesOn (Sum.inl val✝) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (Sum.inl val✝) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (Sum.inl val✝) (fun b ↦ Part.some (g a b)) (h a))

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a ↦
    Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)
a : α
val✝ : γ
⊢ (Option.casesOn (Sum.casesOn (Sum.inr val✝) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (Sum.inr val✝) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (Sum.inr val✝) (fun b ↦ Part.some (g a b)) (h a))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
⊢ Sum.casesOn (Sum.casesOn (f a) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2) (fun b ↦ Part.some (h a b))
      (g a) =
    Sum.casesOn (f a) (g a) fun c ↦ Part.some (h a c)

Tactic:
cases f a

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : β
⊢ Sum.casesOn (Sum.casesOn (Sum.inl val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inl val✝) (g a) fun c ↦ Part.some (h a c)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : γ
⊢ Sum.casesOn (Sum.casesOn (Sum.inr val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inr val✝) (g a) fun c ↦ Part.some (h a c)
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:
· exact Nat.eq_sqrt.2
        ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩

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

Goal state before:
pp: 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
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hnxb : x ≠ b
hxa : Gmax.Adj ↑↑x ↑↑a
hxb : Gmax.Adj ↑↑a ↑↑b
hnadjxb : ¬Gmax.Adj ↑↑x ↑↑b
c : V
hc : ↑↑a ≠ c ∧ ¬Gmax.Adj (↑↑a) c
hbnec : ↑↑b ≠ c
w✝ : (Gmax ⊔ edge ↑↑x ↑↑b).Subgraph
hG1 : w✝.IsPerfectMatching
⊢ ¬?m.343 ≤ Gmax

Tactic:
rwa [edge_le_iff (v := a.1.1) (w := c), not_or]

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

Goal state before:
pp: case one
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z ↦ p * z ^ (p - 1)

pp: case two
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z ↦ p * z ^ (p - 1)

Tactic:
case one => calc
        (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring

Goal state after:
case two
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z ↦ p * z ^ (p - 1)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε ↑n

Tactic:
filter_upwards [eventually_one_sub_smoothingFn_pos] with n hn

Goal state after:
n : ℕ
hn : 0 < 1 - ε ↑n
⊢ 0 ≤ 1 - ε ↑n
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)

Tactic:
have h_deriv_q : deriv q =O[atTop] fun x => x ^ ((p a b) - 1) := calc deriv q
    _ = deriv fun x => (fun z => z ^ (p a b)) x * (fun z => 1 - ε z) x := by rfl
    _ =ᶠ[atTop] fun x => deriv (fun z => z ^ (p a b)) x * (1 - ε x) +
          x ^ (p a b) * deriv (fun z => 1 - ε z) x := by
      filter_upwards [eventually_ne_atTop 0, eventually_gt_atTop 1] with x hx hx'
      rw [deriv_fun_mul] <;> aesop
    _ =O[atTop] fun x => x ^ ((p a b) - 1) := by
      refine IsBigO.add ?left ?right
      case left => calc (fun x => deriv (fun z => z ^ (p a b)) x * (1 - ε x))
        _ =O[atTop] fun x => x ^ ((p a b) - 1) * (1 - ε x) :=
          IsBigO.mul (isBigO_deriv_rpow_const_atTop (p a b)) (isBigO_refl _ _)
        _ =O[atTop] fun x => x ^ ((p a b) - 1) * 1 :=
          IsBigO.mul (isBigO_refl _ _) isEquivalent_one_sub_smoothingFn_one.isBigO
        _ = fun x => x ^ ((p a b) - 1) := by ext; rw [mul_one]
      case right => calc (fun x => x ^ (p a b) * deriv (fun z => 1 - ε z) x)
        _ =O[atTop] (fun x => x ^ (p a b) * x⁻¹) :=
          IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_sub_smoothingFn.isBigO
        _ =ᶠ[atTop] fun x => x ^ ((p a b) - 1) := by
          filter_upwards [eventually_gt_atTop 0] with x hx
          rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ q ↑(r i n)

Tactic:
rw [← h₁, sub_le_iff_le_add', ← sub_le_iff_le_add]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1.left
f : ℕ →. ℕ
⊢ ∃ c, c.eval = ↑fun n ↦ (unpair n).1

Tactic:
exact ⟨left, rfl⟩

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
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, c₂ * g ↑n / ↑u ^ (p a b + 1) ≥
    ↑n ^ p a b * ∑ _u ∈ Ico (r i n) n, c₂ * g ↑n / ↑n ^ (p a b + 1)

Tactic:
gcongr with u hu
        · rw [Finset.mem_Ico] at hu
          have := calc 0 < r i n := hrpos_i
                      _ ≤ u := hu.1
          positivity
        · rw [Finset.mem_Ico] at hu
          exact le_of_lt hu.2

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < T n

pp: case refine_3
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n

Tactic:
· exact Eventually.of_forall fun h => R.T_pos _

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L✝ : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
z✝¹ : Primrec fun a ↦ (unpair a.1.1.2).1
L : Primrec fun a ↦ a.1.1.1.1
z✝ : Primrec fun a ↦ (unpair a.1.1.1.2).1
y✝ : Primrec Prod.snd
h₁ :
  Primrec fun a ↦
    lup (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.2
z : Primrec fun a ↦ (unpair a.1.1.1.1.2).1
y : Primrec fun a ↦ a.1.2
⊢ Primrec fun p ↦
    (fun p i ↦
        lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1)
          (Nat.pair (unpair p.1.1.1.2).1 (Nat.pair p.2 i)))
      p.1 p.2

Tactic:
have i := Primrec.snd
      (α := (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ)
      (β := ℕ)

Goal state after:
case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L✝ : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
z✝¹ : Primrec fun a ↦ (unpair a.1.1.2).1
L : Primrec fun a ↦ a.1.1.1.1
z✝ : Primrec fun a ↦ (unpair a.1.1.1.2).1
y✝ : Primrec Prod.snd
h₁ :
  Primrec fun a ↦
    lup (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.2
z : Primrec fun a ↦ (unpair a.1.1.1.1.2).1
y : Primrec fun a ↦ a.1.2
i : Primrec Prod.snd
⊢ Primrec fun p ↦
    (fun p i ↦
        lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1)
          (Nat.pair (unpair p.1.1.1.2).1 (Nat.pair p.2 i)))
      p.1 p.2
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)) =
    match Fin.ofNat 4 (n + 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
← show Fin.ofNat 4 1 = (1 : ℕ) from Fin.val_ofNat ..

Goal state after:
case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)) =
    match Fin.ofNat 4 (n + ↑(Fin.ofNat 4 1)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Computability.NFA

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

Tactic:
induction x generalizing S T with

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

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ ¬l.reduceOption.length = l.length ↔ none ∈ l

Tactic:
reduceOption_length_eq_iff

Goal state after:
α : Type u_1
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
ih : ∃ t ∈ S, s✝ ∈ M.εClosure {t}
⊢ ∃ t ∈ S, t✝ ∈ M.εClosure {t}

Tactic:
| step _ _ _ _ ih =>

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

Goal state before:
pp: ⊢ ofNat' 1 = 1

Tactic:
simp [Num.ofNat', Num.bit1]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
ih : ∃ n, M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)

Tactic:
| step _ _ _ _ ih =>

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left✝ : x'.reduceOption = x
n : ℕ
h : M.IsPath s₁ s₂ (x' ++ some a :: List.replicate n none)
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
rw [isPath_append] at h

Goal state after:
case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left✝ : x'.reduceOption = x
n : ℕ
h : ∃ t, M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
⊢ (bif Sum.casesOn (f a) (fun b ↦ true) fun b ↦ false then
      Sum.casesOn (f a) (fun b ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun c ↦ Part.some Option.none
    else Sum.casesOn (f a) (fun b ↦ Part.some Option.none) fun b ↦ Part.map Option.some (h (a, b).1 (a, b).2)) =
    Part.map Option.some (Sum.casesOn (f a) (g a) (h a))

Tactic:
cases f a

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val✝ : β
⊢ (bif Sum.casesOn (Sum.inl val✝) (fun b ↦ true) fun b ↦ false then
      Sum.casesOn (Sum.inl val✝) (fun b ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun c ↦ Part.some Option.none
    else
      Sum.casesOn (Sum.inl val✝) (fun b ↦ Part.some Option.none) fun b ↦ Part.map Option.some (h (a, b).1 (a, b).2)) =
    Part.map Option.some (Sum.casesOn (Sum.inl val✝) (g a) (h a))

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val✝ : γ
⊢ (bif Sum.casesOn (Sum.inr val✝) (fun b ↦ true) fun b ↦ false then
      Sum.casesOn (Sum.inr val✝) (fun b ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun c ↦ Part.some Option.none
    else
      Sum.casesOn (Sum.inr val✝) (fun b ↦ Part.some Option.none) fun b ↦ Part.map Option.some (h (a, b).1 (a, b).2)) =
    Part.map Option.some (Sum.casesOn (Sum.inr val✝) (g a) (h a))
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inr
σ₁ : 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₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b✝ e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
d' : σ₂
cd' : d' ∈ f₂ b✝
de : ReflTransGen (fun a b ↦ b ∈ f₂ a) d' e₂
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
cases Option.mem_unique cd cd'
      exact ⟨_, _, de, ee, ae⟩

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

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ = branch p q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
rcases h₁₂ with (rfl | h₁₂ | h₁₂)

Goal state after:
case branch.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)