Theorem: LO.FirstOrder.Arith.omegaOne.mem_iff (Arithmetization/OmegaOne/Basic.lean)

State before:
σ : Sentence ℒₒᵣ
⊢ σ ∈ 𝛀₁ → σ = omegaOneAxiom
Tactic:
rintro ⟨⟩
State after:
case omega

⊢ omegaOneAxiom = omegaOneAxiom

State before:
case omega

⊢ omegaOneAxiom = omegaOneAxiom
Tactic:
rfl
State after:
no goals

State before:
σ : Sentence ℒₒᵣ
⊢ σ = omegaOneAxiom → σ ∈ 𝛀₁
Tactic:
rintro rfl
State after:
⊢ omegaOneAxiom ∈ 𝛀₁

State before:
⊢ omegaOneAxiom ∈ 𝛀₁
Tactic:
exact Theory.omegaOne.omega
State after:
no goals