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

State before:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m (Arith.ballIn t p) ↔ Hierarchy Γ m p
Tactic:
simp only [Arith.ballIn, Rew.bshift_positive, Hierarchy.ball_iff, Hierarchy.imp_iff, and_iff_right_iff_imp]
State after:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m
      (Semiformula.ballLT 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.ballLT 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