Theorem: ReflTransGen.cases_tail_eq_neq (Pdl/Star.lean)

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
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

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
State after:
case refl.h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = z

State before:
case refl.h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = z
Tactic:
rfl
State after:
no goals

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)
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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)
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals