L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n : ℕ
φ : BoundedFormula L α n
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) φ =
    castLE (_ : 0 + n ≥ n) φ
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n : ℕ
φ : BoundedFormula L α n
⊢ relabel Sum.inl φ = castLE (_ : 0 + n ≥ n) φ
simp only [relabel, relabelAux_sum_inl]
case falsum
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) falsum =
    castLE (_ : 0 + n✝ ≥ n✝) falsum

case equal
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (equal t₁✝ t₂✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (equal t₁✝ t₂✝)

case rel
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (rel R✝ ts✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (rel R✝ ts✝)

case imp
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f₁✝ =
    castLE (_ : 0 + n✝ ≥ n✝) f₁✝
ih2 :
  mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f₂✝ =
    castLE (_ : 0 + n✝ ≥ n✝) f₂✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (imp f₁✝ f₂✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (imp f₁✝ f₂✝)

case all
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 :
  mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f✝ =
    castLE (_ : 0 + (n✝ + 1) ≥ n✝ + 1) f✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (all f✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (all f✝)
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n : ℕ
φ : BoundedFormula L α n
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) φ =
    castLE (_ : 0 + n ≥ n) φ
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
no goals
case falsum
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) falsum =
    castLE (_ : 0 + n✝ ≥ n✝) falsum
rfl
no goals
case equal
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (equal t₁✝ t₂✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (equal t₁✝ t₂✝)
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
case rel
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ (fun i => Term.relabel (Sum.map id ↑(Fin.cast (_ : n✝ = 0 + n✝))) (ts✝ i)) =
    Term.relabel (Sum.map id ↑(Fin.cast (_ : n✝ = 0 + n✝))) ∘ ts✝
case rel
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (rel R✝ ts✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (rel R✝ ts✝)
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
no goals
case rel
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ (fun i => Term.relabel (Sum.map id ↑(Fin.cast (_ : n✝ = 0 + n✝))) (ts✝ i)) =
    Term.relabel (Sum.map id ↑(Fin.cast (_ : n✝ = 0 + n✝))) ∘ ts✝
rfl
no goals
case imp
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f₁✝ =
    castLE (_ : 0 + n✝ ≥ n✝) f₁✝
ih2 :
  mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f₂✝ =
    castLE (_ : 0 + n✝ ≥ n✝) f₂✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (imp f₁✝ f₂✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (imp f₁✝ f₂✝)
simp [mapTermRel, ih1, ih2]
no goals
case all
L : Language
L' : Language
M : Type w
N : Type ?u.98243
P : Type ?u.98246
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.98274
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 :
  mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f✝ =
    castLE (_ : 0 + (n✝ + 1) ≥ n✝ + 1) f✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id ↑(natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (all f✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (all f✝)
simp [mapTermRel, ih3, castLE]