Theorem: LO.FirstOrder.UFormula.bindq_param_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
⊢ ∀ (b b' : σ × ℕ × UFormula L μ₁), b' ∈ LO.FirstOrder.UFormula.bindqL b → b'.2.2.depth < b.2.2.depth
Tactic:
rintro ⟨x₁, m₁, p₁⟩ ⟨x₂, m₂, p₂⟩
State after:
case mk.mk.mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
p₁ : UFormula L μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈ LO.FirstOrder.UFormula.bindqL (x₁, m₁, p₁) → (x₂, m₂, p₂).2.2.depth < (x₁, m₁, p₁).2.2.depth

State before:
case mk.mk.mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
p₁ : UFormula L μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈ LO.FirstOrder.UFormula.bindqL (x₁, m₁, p₁) → (x₂, m₂, p₂).2.2.depth < (x₁, m₁, p₁).2.2.depth
Tactic:
simp[bindqL]
State after:
case mk.mk.mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
p₁ : UFormula L μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈
      Sum.rec (fun val => [])
        (fun val =>
          Sum.rec (fun val => [])
            (fun val =>
              Sum.rec (fun val => List.map (fun x => (x₁, m₁, x)) p₁.inversion.2)
                (fun val => List.map (fun x => (x₁, m₁ + 1, x)) p₁.inversion.2) val)
            val)
        p₁.inversion.1.2 →
    p₂.depth < p₁.depth

State before:
case mk.mk.mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
p₁ : UFormula L μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈
      Sum.rec (fun val => [])
        (fun val =>
          Sum.rec (fun val => [])
            (fun val =>
              Sum.rec (fun val => List.map (fun x => (x₁, m₁, x)) p₁.inversion.2)
                (fun val => List.map (fun x => (x₁, m₁ + 1, x)) p₁.inversion.2) val)
            val)
        p₁.inversion.1.2 →
    p₂.depth < p₁.depth
Tactic:
cases p₁ <;> simp[inversion]
State after:
case mk.mk.mk.mk.and
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.and a✝).depth

case mk.mk.mk.mk.or
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.or a✝).depth

case mk.mk.mk.mk.all
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.all.depth

case mk.mk.mk.mk.ex
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.ex.depth

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.and a✝).depth
Tactic:
case and => rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.or a✝).depth
Tactic:
case or => rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.all.depth
Tactic:
case all => rintro rfl rfl rfl; simp[depth]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.ex.depth
Tactic:
case ex => rintro rfl rfl rfl; simp[depth]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.and a✝).depth
Tactic:
rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.or a✝).depth
Tactic:
rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.all.depth
Tactic:
rintro rfl rfl rfl
State after:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.all.depth

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.all.depth
Tactic:
simp[depth]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.ex.depth
Tactic:
rintro rfl rfl rfl
State after:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.ex.depth

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.ex.depth
Tactic:
simp[depth]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
⊢ ∀ (b_1 : σ × ℕ × UFormula L μ₁),
    LO.FirstOrder.UFormula.bindqG b e b_1
        (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (LO.FirstOrder.UFormula.bindqL b_1)) =
      some ((fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) b_1)
Tactic:
rintro ⟨x, m, p⟩
State after:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (LO.FirstOrder.UFormula.bindqL (x, m, p))) =
    some ((fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (x, m, p))

State before:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (LO.FirstOrder.UFormula.bindqL (x, m, p))) =
    some ((fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (x, m, p))
Tactic:
simp[bindqL]
State after:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2)
        (Sum.rec (fun val => [])
          (fun val =>
            Sum.rec (fun val => [])
              (fun val =>
                Sum.rec (fun val => List.map (fun x_1 => (x, m, x_1)) p.inversion.2)
                  (fun val => List.map (fun x_1 => (x, m + 1, x_1)) p.inversion.2) val)
              val)
          p.inversion.1.2)) =
    some (bindq (b x) (e x) m p)

State before:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2)
        (Sum.rec (fun val => [])
          (fun val =>
            Sum.rec (fun val => [])
              (fun val =>
                Sum.rec (fun val => List.map (fun x_1 => (x, m, x_1)) p.inversion.2)
                  (fun val => List.map (fun x_1 => (x, m + 1, x_1)) p.inversion.2) val)
              val)
          p.inversion.1.2)) =
    some (bindq (b x) (e x) m p)
Tactic:
cases p <;> simp[inversion, bindq, bindqG]
State after:
no goals