Theorem: LO.FirstOrder.System.inconsistent_lMap (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ System.Inconsistent T → System.Inconsistent (Theory.lMap Φ T)
Tactic:
simp [System.inconsistent_iff_provable_bot]
State after:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ T ⊢! ⊥ → Theory.lMap Φ T ⊢! ⊥

State before:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ T ⊢! ⊥ → Theory.lMap Φ T ⊢! ⊥
Tactic:
intro ⟨b⟩
State after:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
b : T ⊢ ⊥
⊢ Theory.lMap Φ T ⊢! ⊥

State before:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
b : T ⊢ ⊥
⊢ Theory.lMap Φ T ⊢! ⊥
Tactic:
exact ⟨by simpa using lMap Φ b⟩
State after:
no goals

State before:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
b : T ⊢ ⊥
⊢ Theory.lMap Φ T ⊢ ⊥
Tactic:
simpa using lMap Φ b
State after:
no goals