Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.fixpoint_eq (Logic/FirstOrder/Incompleteness/SelfReference.lean)

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
⊢ fixpoint θ = ∀' ([→ #0, ⸢diag θ⸣, ⸢diag θ⸣].hom ssbs ⟶ [→ #0].hom θ)
Tactic:
simp [fixpoint, substs_diag]
State after:
no goals