Theorem: LO.Modal.Standard.Kripke.GeachConfluent.transitive_def (Logic/Modal/Standard/Kripke/Geach/Definability.lean)

State before:
α : Sort ?u.51487
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 2, m := 1, n := 0 } F ↔ Transitive F.Rel
Tactic:
simp [GeachConfluent, Transitive]
State after:
α : Sort ?u.51487
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → ∀ (x_1 : F.World), x ≺ x_1 → x_1 ≺ z → y ≺ z) ↔
    ∀ ⦃x y z : F.World⦄, F.Rel x y → F.Rel y z → F.Rel x z

State before:
α : Sort ?u.51487
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → ∀ (x_1 : F.World), x ≺ x_1 → x_1 ≺ z → y ≺ z) ↔
    ∀ ⦃x y z : F.World⦄, F.Rel x y → F.Rel y z → F.Rel x z
Tactic:
aesop
State after:
no goals