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

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

State before:
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) ↔ ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
Tactic:
constructor
State after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) → ∀ ⦃x y : F.World⦄, F.Rel x y → x = y

case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y

State before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) → ∀ ⦃x y : F.World⦄, F.Rel x y → x = y

case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
Tactic:
. intro h x y hyz;
  have := h rfl hyz;
  subst this;
  trivial;
State after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y

State before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
Tactic:
. intro h x y z hxy hxz;
  have := h hxz;
  subst hxy this;
  trivial;
State after:
no goals

State before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) → ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
Tactic:
intro h x y hyz
State after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
⊢ x = y

State before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
⊢ x = y
Tactic:
have := h rfl hyz
State after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
this : y = x
⊢ x = y

State before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
this : y = x
⊢ x = y
Tactic:
subst this
State after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
y : F.World
hyz : F.Rel y y
⊢ y = y

State before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
y : F.World
hyz : F.Rel y y
⊢ y = y
Tactic:
trivial
State after:
no goals

State before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
Tactic:
intro h x y z hxy hxz
State after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
⊢ z = y

State before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
⊢ z = y
Tactic:
have := h hxz
State after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
this : x = z
⊢ z = y

State before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
this : x = z
⊢ z = y
Tactic:
subst hxy this
State after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x : F.World
hxz : x ≺ x
⊢ x = x

State before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x : F.World
hxz : x ≺ x
⊢ x = x
Tactic:
trivial
State after:
no goals