Theorem: logicInIdentity (Fine/Semantics/Satisfaction.lean)

State before:
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g ↔ ∀ (x : α), x⊨f → x⊨g
Tactic:
apply Iff.intro
State after:
case mp
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g → ∀ (x : α), x⊨f → x⊨g

case mpr
α : Type
inst : Model α
f g : Form
⊢ (∀ (x : α), x⊨f → x⊨g) → Model.identity⊨f⊃g

State before:
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g → ∀ (x : α), x⊨f → x⊨g
Tactic:
case mp => 
  intros h₁ x h₂
  rw [←inst.appLeftIdent x]
  exact h₁ h₂
State after:
no goals

State before:
α : Type
inst : Model α
f g : Form
⊢ (∀ (x : α), x⊨f → x⊨g) → Model.identity⊨f⊃g
Tactic:
case mpr =>
  intro h₁ u h₂
  rw [inst.appLeftIdent u]
  exact h₁ u h₂
State after:
no goals

State before:
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g → ∀ (x : α), x⊨f → x⊨g
Tactic:
intros h₁ x h₂
State after:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ x⊨g

State before:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ x⊨g
Tactic:
rw [←inst.appLeftIdent x]
State after:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ Model.identity∙x⊨g

State before:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ Model.identity∙x⊨g
Tactic:
exact h₁ h₂
State after:
no goals

State before:
α : Type
inst : Model α
f g : Form
⊢ (∀ (x : α), x⊨f → x⊨g) → Model.identity⊨f⊃g
Tactic:
intro h₁ u h₂
State after:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ Model.identity∙u⊨g

State before:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ Model.identity∙u⊨g
Tactic:
rw [inst.appLeftIdent u]
State after:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ u⊨g

State before:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ u⊨g
Tactic:
exact h₁ u h₂
State after:
no goals