Theorem: LO.Sound.consistent_of_meaningful (Logic/Logic/System.lean)

State before:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
𝓢 𝓣 : S
𝓜 𝓝 : M
inst✝¹ : Sound 𝓢 𝓜
inst✝ : Sound 𝓣 𝓝
H : Semantics.Meaningful 𝓜
h : System.Inconsistent 𝓢
⊢ False
Tactic:
rcases H with ⟨f, hf⟩
State after:
case mk.intro
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
𝓢 𝓣 : S
𝓜 𝓝 : M
inst✝¹ : Sound 𝓢 𝓜
inst✝ : Sound 𝓣 𝓝
h : System.Inconsistent 𝓢
f : F
hf : ¬𝓜 ⊧ f
⊢ False

State before:
case mk.intro
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
𝓢 𝓣 : S
𝓜 𝓝 : M
inst✝¹ : Sound 𝓢 𝓜
inst✝ : Sound 𝓣 𝓝
h : System.Inconsistent 𝓢
f : F
hf : ¬𝓜 ⊧ f
⊢ False
Tactic:
exact hf (Sound.sound (h f))
State after:
no goals