internlm/Lean-Github huggingface dataset:
Theorem: LO.System.Context.by_axm!
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : DecidableEq F
S : Type u_2
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p : F
Γ : Set F
h : p ∈ Γ
⊢ p ∈ Collection.set { ctx := Γ }
Tactic:
simpa
Proof state after:
no goals
Theorem: serial_of_refl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
⊢ Serial rel
Tactic:
rintro w
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w : α
⊢ ∃ w₂, rel w w₂
Theorem: serial_of_refl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w : α
⊢ ∃ w₂, rel w w₂
Tactic:
existsi w
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w : α
⊢ rel w w
Theorem: serial_of_refl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w : α
⊢ rel w w
Tactic:
exact hRefl w
Proof state after:
no goals
Theorem: eucl_of_symm_trans
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
⊢ Euclidean rel
Tactic:
intro w₁ w₂ w₃ r₁₂ r₁₃
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
⊢ rel w₃ w₂
Theorem: eucl_of_symm_trans
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
⊢ rel w₃ w₂
Tactic:
have r₂₁ := hSymm r₁₂
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
r₂₁ : rel w₂ w₁
⊢ rel w₃ w₂
Theorem: eucl_of_symm_trans
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
r₂₁ : rel w₂ w₁
⊢ rel w₃ w₂
Tactic:
exact hSymm $ hTrans r₂₁ r₁₃
Proof state after:
no goals
Theorem: trans_of_symm_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
⊢ Transitive rel
Tactic:
rintro w₁ w₂ w₃ r₁₂ r₂₃
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₂₃ : rel w₂ w₃
⊢ rel w₁ w₃
Theorem: trans_of_symm_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₂₃ : rel w₂ w₃
⊢ rel w₁ w₃
Tactic:
exact hSymm $ hEucl (hSymm r₁₂) r₂₃
Proof state after:
no goals
Theorem: symm_of_refl_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
⊢ Symmetric rel
Tactic:
intro w₁ w₂ r₁₂
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ : α
r₁₂ : rel w₁ w₂
⊢ rel w₂ w₁
Theorem: symm_of_refl_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ : α
r₁₂ : rel w₁ w₂
⊢ rel w₂ w₁
Tactic:
exact hEucl (hRefl w₁) r₁₂
Proof state after:
no goals
Theorem: trans_of_refl_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
⊢ Transitive rel
Tactic:
have hSymm := symm_of_refl_eucl hRefl hEucl
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm✝ : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
hSymm : Symmetric rel
⊢ Transitive rel
Theorem: trans_of_refl_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm✝ : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
hSymm : Symmetric rel
⊢ Transitive rel
Tactic:
exact trans_of_symm_eucl hSymm hEucl
Proof state after:
no goals
Theorem: refl_of_symm_serial_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
⊢ Reflexive rel
Tactic:
rintro w₁
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ : α
⊢ rel w₁ w₁
Theorem: refl_of_symm_serial_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ : α
⊢ rel w₁ w₁
Tactic:
obtain ⟨w₂, r₁₂⟩ := hSerial w₁
Proof state after:
case intro
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ : α
r₁₂ : rel w₁ w₂
⊢ rel w₁ w₁
Theorem: refl_of_symm_serial_eucl
Proof state before:
case intro
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ : α
r₁₂ : rel w₁ w₂
⊢ rel w₁ w₁
Tactic:
have r₂₁ := hSymm r₁₂
Proof state after:
case intro
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ : α
r₁₂ : rel w₁ w₂
r₂₁ : rel w₂ w₁
⊢ rel w₁ w₁
Theorem: refl_of_symm_serial_eucl
Proof state before:
case intro
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ : α
r₁₂ : rel w₁ w₂
r₂₁ : rel w₂ w₁
⊢ rel w₁ w₁
Tactic:
exact trans_of_symm_eucl hSymm hEucl r₁₂ r₂₁
Proof state after:
no goals
Theorem: ConverseWellFounded.iff_has_max
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
r : α → α → Prop
⊢ ConverseWellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r m x
Tactic:
simp [ConverseWellFounded, WellFounded.wellFounded_iff_has_min, flip]
Proof state after:
no goals
Theorem: Finite.converseWellFounded_of_trans_irrefl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
⊢ ConverseWellFounded rel
Tactic:
apply @Finite.wellFounded_of_trans_of_irrefl _ _ _
  ⟨by intro a b c rba rcb; exact IsTrans.trans c b a rcb rba⟩
  ⟨by simp [flip, IsIrrefl.irrefl]⟩
Proof state after:
no goals
Theorem: Finite.converseWellFounded_of_trans_irrefl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
⊢ ∀ (a b c : α),
    flip (fun x x_1 => rel x x_1) a b → flip (fun x x_1 => rel x x_1) b c → flip (fun x x_1 => rel x x_1) a c
Tactic:
intro a b c rba rcb
Proof state after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
a b c : α
rba : flip (fun x x_1 => rel x x_1) a b
rcb : flip (fun x x_1 => rel x x_1) b c
⊢ flip (fun x x_1 => rel x x_1) a c
Theorem: Finite.converseWellFounded_of_trans_irrefl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
a b c : α
rba : flip (fun x x_1 => rel x x_1) a b
rcb : flip (fun x x_1 => rel x x_1) b c
⊢ flip (fun x x_1 => rel x x_1) a c
Tactic:
exact IsTrans.trans c b a rcb rba
Proof state after:
no goals
Theorem: Finite.converseWellFounded_of_trans_irrefl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
⊢ ∀ (a : α), ¬flip (fun x x_1 => rel x x_1) a a
Tactic:
simp [flip, IsIrrefl.irrefl]
Proof state after:
no goals
Theorem: extensive_of_reflex_antisymm_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
⊢ Extensive rel
Tactic:
intro x y rxy
Proof state after:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
⊢ x = y
Theorem: extensive_of_reflex_antisymm_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
⊢ x = y
Tactic:
have rxx := hRefl x
Proof state after:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
rxx : rel x x
⊢ x = y
Theorem: extensive_of_reflex_antisymm_eucl
Proof state before:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
rxx : rel x x
⊢ x = y
Tactic:
exact hAntisymm rxy (hEucl rxx rxy)
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ F ⊧* 𝗟 → Transitive F.Rel
Tactic:
contrapose
Proof state after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬Transitive F.Rel → ¬F ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬Transitive F.Rel → ¬F ⊧* 𝗟
Tactic:
intro hT
Proof state after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ¬Transitive F.Rel
⊢ ¬F ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ¬Transitive F.Rel
⊢ ¬F ⊧* 𝗟
Tactic:
simp [Transitive] at hT
Proof state after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x_1 x_2 ∧ ¬F.Rel x x_2
⊢ ¬F ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x_1 x_2 ∧ ¬F.Rel x x_2
⊢ ¬F ⊧* 𝗟
Tactic:
obtain ⟨w₁, w₂, r₁₂, w₃, r₂₃, nr₁₃⟩ := hT
Proof state after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ¬F ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ¬F ⊧* 𝗟
Tactic:
simp only [Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff, ValidOnFrame,
  ValidOnModel.iff_models, ValidOnModel, Satisfies.iff_models, forall_exists_index,
  forall_apply_eq_imp_iff, Satisfies.imp_def, Satisfies.box_def, not_forall, exists_prop]
Proof state after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∃ x x_1 x_2,
    (∀ (w' : F.World),
        x_2 ≺ w' →
          (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := x_1 } w'_1 x) →
            Satisfies { Frame := F, Valuation := x_1 } w' x) ∧
      ∃ x_3, x_2 ≺ x_3 ∧ ¬Satisfies { Frame := F, Valuation := x_1 } x_3 x
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∃ x x_1 x_2,
    (∀ (w' : F.World),
        x_2 ≺ w' →
          (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := x_1 } w'_1 x) →
            Satisfies { Frame := F, Valuation := x_1 } w' x) ∧
      ∃ x_3, x_2 ≺ x_3 ∧ ¬Satisfies { Frame := F, Valuation := x_1 } x_3 x
Tactic:
existsi (atom default), (λ w' _ => w' ≠ w₂ ∧ w' ≠ w₃), w₁
Proof state after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ (∀ (w' : F.World),
      w₁ ≺ w' →
        (∀ (w'_1 : F.World),
            w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
          Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)) ∧
    ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ (∀ (w' : F.World),
      w₁ ≺ w' →
        (∀ (w'_1 : F.World),
            w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
          Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)) ∧
    ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∀ (w' : F.World),
    w₁ ≺ w' →
      (∀ (w'_1 : F.World),
          w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)

case intro.intro.intro.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case intro.intro.intro.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∀ (w' : F.World),
    w₁ ≺ w' →
      (∀ (w'_1 : F.World),
          w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)

case intro.intro.intro.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. intro x hx h;
  by_cases hx₂ : x = w₂;
  . subst hx₂; simpa [Satisfies] using h w₃ r₂₃;
  . by_cases hx₃ : x = w₃ <;> simp_all [Satisfies, hx₃];
Proof state after:
case intro.intro.intro.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case intro.intro.intro.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. existsi w₂; simpa [Satisfies];
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case intro.intro.intro.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∀ (w' : F.World),
    w₁ ≺ w' →
      (∀ (w'_1 : F.World),
          w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
Tactic:
intro x hx h
Proof state after:
case intro.intro.intro.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case intro.intro.intro.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
by_cases hx₂ : x = w₂
Proof state after:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. subst hx₂; simpa [Satisfies] using h w₃ r₂₃;
Proof state after:
case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. by_cases hx₃ : x = w₃ <;> simp_all [Satisfies, hx₃];
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
subst hx₂
Proof state after:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₃ : F.World
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
r₁₂ : F.Rel w₁ x
r₂₃ : F.Rel x w₃
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } x (atom default)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₃ : F.World
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
r₁₂ : F.Rel w₁ x
r₂₃ : F.Rel x w₃
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } x (atom default)
Tactic:
simpa [Satisfies] using h w₃ r₂₃
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof state before:
case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
by_cases hx₃ : x = w₃ <;> simp_all [Satisfies, hx₃]
Proof state after:
no goals