internlm/Lean-Github huggingface dataset:
Theorem: mytaut1
Proof state before:
p : Char
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    match (M, w), (·p)↣·p with
    | (fst, snd), Formula.bottom => False
    | (M, w), ·p => M.val w p
    | (M, w), ~φ => ¬Evaluate (M, w) φ
    | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
    | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
intro W M w
Proof state after:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Theorem: mytaut1
Proof state before:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
simp
Proof state after:
no goals
Theorem: mytaut2
Proof state before:
p : Char
⊢ Tautology ((~~·p)↣·p)
Tactic:
unfold Tautology Evaluate
Proof state after:
p : Char
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    match (M, w), (~~·p)↣·p with
    | (fst, snd), Formula.bottom => False
    | (M, w), ·p => M.val w p
    | (M, w), ~φ => ¬Evaluate (M, w) φ
    | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
    | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Theorem: mytaut2
Proof state before:
p : Char
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    match (M, w), (~~·p)↣·p with
    | (fst, snd), Formula.bottom => False
    | (M, w), ·p => M.val w p
    | (M, w), ~φ => ¬Evaluate (M, w) φ
    | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
    | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
intro W M w
Proof state after:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (~~·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Theorem: mytaut2
Proof state before:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (~~·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
classical
simp
Proof state after:
no goals
Theorem: mytaut2
Proof state before:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (~~·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
simp
Proof state after:
no goals
Theorem: mysat
Proof state before:
p : Char
⊢ Satisfiable (·p)
Tactic:
unfold Satisfiable
Proof state after:
p : Char
⊢ formHasSat.1 (·p)
Theorem: mysat
Proof state before:
p : Char
⊢ formHasSat.1 (·p)
Tactic:
exists ℕ
Proof state after:
p : Char
⊢ ∃ M w, Evaluate (M, w) (·p)
Theorem: mysat
Proof state before:
p : Char
⊢ ∃ M w, Evaluate (M, w) (·p)
Tactic:
exists myModel
Proof state after:
p : Char
⊢ ∃ w, Evaluate (myModel, w) (·p)
Theorem: mysat
Proof state before:
p : Char
⊢ ∃ w, Evaluate (myModel, w) (·p)
Tactic:
exists 1
Proof state after:
no goals
Theorem: boxTop
Proof state before:
⊢ Tautology (□⊤)
Tactic:
unfold Tautology Evaluate
Proof state after:
⊢ ∀ (W : Type) (M : KripkeModel W) (w v : W), M.Rel w v → Evaluate (M, v) ⊤
Theorem: boxTop
Proof state before:
⊢ ∀ (W : Type) (M : KripkeModel W) (w v : W), M.Rel w v → Evaluate (M, v) ⊤
Tactic:
tauto
Proof state after:
no goals
Theorem: A3
Proof state before:
X Y : Formula
⊢ Tautology (□(X⋀Y)↣□X⋀□Y)
Tactic:
simp_all [Tautology, Evaluate]
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
h : Relation.ReflTransGen r x z
⊢ x = z ∨ x ≠ z ∧ ∃ y, x ≠ y ∧ r x y ∧ Relation.ReflTransGen r y z
Tactic:
induction h using Relation.ReflTransGen.head_induction_on
Proof state after:
case refl
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = z ∨ z ≠ z ∧ ∃ y, z ≠ y ∧ r z y ∧ Relation.ReflTransGen r y z

case head
α : Type u_1
x z : α
r : α → α → Prop
a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : Relation.ReflTransGen r c✝ z
a✝ : c✝ = z ∨ c✝ ≠ z ∧ ∃ y, c✝ ≠ y ∧ r c✝ y ∧ Relation.ReflTransGen r y z
⊢ a✝¹ = z ∨ a✝¹ ≠ z ∧ ∃ y, a✝¹ ≠ y ∧ r a✝¹ y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case refl
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = z ∨ z ≠ z ∧ ∃ y, z ≠ y ∧ r z y ∧ Relation.ReflTransGen r y z
Tactic:
left
Proof state after:
case refl.h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case refl.h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = z
Tactic:
rfl
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
IH_b_z : b = z ∨ b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
cases Classical.em (a = b)
Proof state after:
case inl
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
IH_b_z : b = z ∨ b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : a = b
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z

case inr
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
IH_b_z : b = z ∨ b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = b
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
IH_b_z : b = z ∨ b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
a_is_b : a = b
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
case inl a_is_b =>
  subst a_is_b
  cases IH_b_z
  case inl a_is_z =>
    left
    assumption
  case inr IH =>
    right
    assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
IH_b_z : b = z ∨ b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
a_is_b : a = b
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
subst a_is_b
Proof state after:
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
IH_b_z : a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
IH_b_z : a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
cases IH_b_z
Proof state after:
case inl
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
h✝ : a = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z

case inr
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
h✝ : a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
a_is_z : a = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
case inl a_is_z =>
  left
  assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
IH : a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
case inr IH =>
  right
  assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
a_is_z : a = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
left
Proof state after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
a_is_z : a = z
⊢ a = z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
a_is_z : a = z
⊢ a = z
Tactic:
assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
IH : a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
right
Proof state after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
IH : a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
⊢ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a : α
a_r_b : r a a
b_r_z : Relation.ReflTransGen r a z
IH : a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
⊢ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
IH_b_z : b = z ∨ b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
a_neq_b : ¬a = b
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
cases IH_b_z
Proof state after:
case inl
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
h✝ : b = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z

case inr
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
h✝ : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
a_is_z : b = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
subst a_is_z
Proof state after:
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ a = b ∨ a ≠ b ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y b
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ a = b ∨ a ≠ b ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y b
Tactic:
right
Proof state after:
case h
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ a ≠ b ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y b
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case h
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ a ≠ b ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y b
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ a ≠ b

case h.right
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y b
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case h.left
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ a ≠ b
Tactic:
assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case h.right
α : Type u_1
x : α
r : α → α → Prop
a b : α
a_r_b : r a b
a_neq_b : ¬a = b
b_r_z : Relation.ReflTransGen r b b
⊢ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y b
Tactic:
use b
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
cases Classical.em (a = z)
Proof state after:
case inl
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : a = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z

case inr
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case inl
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : a = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
left
Proof state after:
case inl.h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : a = z
⊢ a = z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case inl.h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : a = z
⊢ a = z
Tactic:
assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case inr
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
right
Proof state after:
case inr.h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case inr.h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
constructor
Proof state after:
case inr.h.left
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ a ≠ z

case inr.h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case inr.h.left
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ a ≠ z
Tactic:
assumption
Proof state after:
no goals
Theorem: ReflTransGen.cases_tail_eq_neq
Proof state before:
case inr.h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
IH : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
h✝ : ¬a = z
⊢ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
Tactic:
use b
Proof state after:
no goals
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
h : Relation.ReflTransGen r x z
⊢ ∃ n ys, x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
induction h using Relation.ReflTransGen.head_induction_on
Proof state after:
case refl
α : Type u_1
x z : α
r : α → α → Prop
⊢ ∃ n ys, z = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)

case head
α : Type u_1
x z : α
r : α → α → Prop
a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : Relation.ReflTransGen r c✝ z
a✝ : ∃ n ys, c✝ = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ∃ n ys, a✝¹ = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
⊢ ∃ n ys, z = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
case refl =>
  use 0, Vector.cons z Vector.nil
  aesop
Proof state after:
no goals
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
⊢ ∃ n ys, z = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
use 0, Vector.cons z Vector.nil
Proof state after:
case h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = (z ::ᵥ Vector.nil).head ∧
    z = (z ::ᵥ Vector.nil).last ∧ ∀ (i : Fin 0), r ((z ::ᵥ Vector.nil).get i.castSucc) ((z ::ᵥ Vector.nil).get i.succ)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = (z ::ᵥ Vector.nil).head ∧
    z = (z ::ᵥ Vector.nil).last ∧ ∀ (i : Fin 0), r ((z ::ᵥ Vector.nil).get i.castSucc) ((z ::ᵥ Vector.nil).get i.succ)
Tactic:
aesop
Proof state after:
no goals
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
IH_b_z : ∃ n ys, b = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ∃ n ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
rcases IH_b_z with ⟨m, zs, b_is_head_zs, z_is_last_zs, zs_steps⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ n ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case intro.intro.intro.intro
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ n ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
use m + 1
Proof state after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin (m + 1)), r (ys.get i.castSucc) (ys.get i.succ)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin (m + 1)), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
use a ::ᵥ zs
Proof state after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ a = (a ::ᵥ zs).head ∧ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) ((a ::ᵥ zs).get i.succ)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ a = (a ::ᵥ zs).head ∧ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) ((a ::ᵥ zs).get i.succ)
Tactic:
simp only [Vector.head_cons, Vector.get_cons_succ, true_and]
Proof state after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last

case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h.left
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last
Tactic:
aesop
Proof state after:
no goals
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Tactic:
intro i
Proof state after:
case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i : Fin (m + 1)
⊢ r ((a ::ᵥ zs).get i.castSucc) (zs.get i)