Theorem: LO.FirstOrder.Arith.Hieralchy.bexIn (Arithmetization/ISigmaOne/Bit.lean)

State before:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m (Arith.bexIn t p) ↔ Hierarchy Γ m p
Tactic:
simp only [Arith.bexIn, Rew.bshift_positive, Hierarchy.bex_iff, Hierarchy.and_iff, and_iff_right_iff_imp]
State after:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m
      (Semiformula.bexLT t
        (“(#0 ∈ !!(Rew.bShift t) ∧ !((Rew.substs (#0 :> fun x => #(BinderNotation.finSuccItr x 1))).hom p))”)) ↔
    Hierarchy Γ m p

State before:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m
      (Semiformula.bexLT t
        (“(#0 ∈ !!(Rew.bShift t) ∧ !((Rew.substs (#0 :> fun x => #(BinderNotation.finSuccItr x 1))).hom p))”)) ↔
    Hierarchy Γ m p
Tactic:
simp [Semiformula.Operator.operator, operator_mem_def]
State after:
no goals