Theorem: not_joins_a_d (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬joins RX X.a X.d
Tactic:
intros h
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : joins RX X.a X.d
⊢ False

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : joins RX X.a X.d
⊢ False
Tactic:
cases' h with w h
State after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h : refl_trans_clos RX X.a w ∧ refl_trans_clos RX X.d w
⊢ False

State before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h : refl_trans_clos RX X.a w ∧ refl_trans_clos RX X.d w
⊢ False
Tactic:
cases' h with h1 h2
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
⊢ False

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
⊢ False
Tactic:
have eq_a : X.a = w := by
  apply normal_red RX <;> aesop
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
⊢ False

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
⊢ False
Tactic:
have eq_d : X.d = w := by
  apply normal_red RX <;> aesop
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
eq_d : X.d = w
⊢ False

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
eq_d : X.d = w
⊢ False
Tactic:
simp [← eq_a] at eq_d
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
⊢ X.a = w
Tactic:
apply normal_red RX <;> aesop
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
⊢ X.d = w
Tactic:
apply normal_red RX <;> aesop
State after:
no goals