Theorem: semEquiv.transitive (Bml/Semantics.lean)

State before:
⊢ Transitive semEquiv
Tactic:
unfold Transitive
State after:
⊢ ∀ ⦃x y z : Formula⦄, semEquiv x y → semEquiv y z → semEquiv x z

State before:
⊢ ∀ ⦃x y z : Formula⦄, semEquiv x y → semEquiv y z → semEquiv x z
Tactic:
unfold semEquiv
State after:
⊢ ∀ ⦃x y z : Formula⦄,
    (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) x ↔ Evaluate (M, w) y) →
      (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) y ↔ Evaluate (M, w) z) →
        ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) x ↔ Evaluate (M, w) z

State before:
⊢ ∀ ⦃x y z : Formula⦄,
    (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) x ↔ Evaluate (M, w) y) →
      (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) y ↔ Evaluate (M, w) z) →
        ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) x ↔ Evaluate (M, w) z
Tactic:
intro f g h f_is_g g_is_h W M w
State after:
f g h : Formula
f_is_g : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h

State before:
f g h : Formula
f_is_g : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Tactic:
specialize f_is_g W M w
State after:
f g h : Formula
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h

State before:
f g h : Formula
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Tactic:
specialize g_is_h W M w
State after:
f g h : Formula
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : Evaluate (M, w) g ↔ Evaluate (M, w) h
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h

State before:
f g h : Formula
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : Evaluate (M, w) g ↔ Evaluate (M, w) h
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Tactic:
tauto
State after:
no goals