Theorem: LO.System.LoebRule.loeb! (Logic/Modal/Standard/HilbertStyle.lean)

State before:
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : LoebRule 𝓢
⊢ 𝓢 ⊢! □p ⟶ p → 𝓢 ⊢! p
Tactic:
rintro ⟨hp⟩
State after:
case intro
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : LoebRule 𝓢
hp : 𝓢 ⊢ □p ⟶ p
⊢ 𝓢 ⊢! p

State before:
case intro
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : LoebRule 𝓢
hp : 𝓢 ⊢ □p ⟶ p
⊢ 𝓢 ⊢! p
Tactic:
exact ⟨loeb hp⟩
State after:
no goals