Hierarchy of is Sigma1

lemma hierarchy_of_isSigma1 {n : ℕ} (ψ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ n) :    IsSigma1 (⌜ψ⌝ : ℕ) → Hierarchy 𝚺 1 ψ := by  induction ψ using Semiformula.rec' with  | hverum => intro _; simp  | hfalsum => intro _; simp  | hrel R v => intro _; exact Hierarchy.rel _ _ _ _  | hnrel R v => intro _; exact Hierarchy.nrel _ _ _ _  | hand φ ψ ihφ ihψ =>      intro h; rw [Semiformula.quote_and (V := ℕ) φ ψ, IsSigma1.and_iff] at h      exact Hierarchy.and (ihφ h.1) (ihψ h.2)  | hor φ ψ ihφ ihψ =>      intro h; rw [Semiformula.quote_or (V := ℕ) φ ψ, IsSigma1.or_iff] at h      exact Hierarchy.or (ihφ h.1) (ihψ h.2)  | hall φ ihφ =>      intro h      rw [Semiformula.quote_all (V := ℕ) φ] at h      obtain ⟨u, q, ⟨t, ht, rfl⟩, hq, hφeq⟩ := IsSigma1.of_all h      have hsf := Semiformula.quote_isSemiformula (V := ℕ) φ      simp only [natCast_nat] at hsf      rw [hφeq, Arithmetic.qqNLT] at hsf      simp only [IsSemiformula.or, IsSemiformula.nrel] at hsf      obtain ⟨⟨_, hvec⟩, hqsf⟩ := hsf      obtain ⟨φ₂, hφ₂⟩ := Bootstrapping.IsSemiformula.sound hqsf      have htmsf := hvec.nth (i := 1) (show (1 : ℕ) < 2 by simp)      simp only [nth_adjoin_one, nth_adjoin_zero] at htmsf      obtain ⟨s, hs⟩ := Bootstrapping.IsSemiterm.sound        ((IsSemiterm.def (L := ℒₒᵣ)).mpr ⟨ht,          (termBV_termBShift_le (L := ℒₒᵣ) ht _).mp ((IsSemiterm.def (L := ℒₒᵣ)).mp htmsf).2⟩)      have heq : (∀¹ φ) = ∀¹[“#0 < !!(Rew.bShift s)”] φ₂ := by        apply (Semiformula.quote_inj_iff (L := ℒₒᵣ) (V := ℕ)).mp        rw [Semiformula.quote_all (V := ℕ) φ, hφeq, quote_ball, hs, hφ₂]        rfl      have hφ : Hierarchy 𝚺 1 φ := ihφ (by rw [hφeq]; simp [IsSigma1.or_iff, hq, Arithmetic.qqNLT])      have hφ2 : Hierarchy 𝚺 1 φ₂ := by        have hform : φ = (“#0 < !!(Rew.bShift s)” 🡒 φ₂) :=          (Semiformula.all_inj _ _).mp (by rw [← Semiformula.ball_eq]; exact heq)        rw [hform, Semiformula.imp_eq, Hierarchy.or_iff] at hφ        exact hφ.2      rw [heq]      exact Hierarchy.ball (Rew.positive_iff.mpr ⟨s, rfl⟩) hφ2  | hexs φ ihφ =>      intro h; rw [Semiformula.quote_ex (V := ℕ) φ, IsSigma1.ex_iff] at h      exact Hierarchy.exs (ihφ h)