Theorem: inc_refl_trans_confl (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => R x x_1) fun x x_1 => S x x_1) →
    ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => S x x_1) fun x x_1 => refl_trans_clos R x x_1) →
      confluent S → confluent R
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) → (∀ (x y : A), S x y → refl_trans_clos R x y) → confluent S → confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) → (∀ (x y : A), S x y → refl_trans_clos R x y) → confluent S → confluent R
Tactic:
intros
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent R
Tactic:
apply (conf_trans_clos _).1
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent (refl_trans_clos R)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent (refl_trans_clos R)
Tactic:
apply equiv_conf
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), ?S x y ↔ refl_trans_clos R x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent ?S

case S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), ?S x y ↔ refl_trans_clos R x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent ?S

case S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Tactic:
. apply inc_refl_trans_eq; simp
  . trivial
  . simp; trivial
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent fun x y => (fun x x_1 => refl_trans_clos (fun x y => S x y) x x_1) x y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent fun x y => (fun x x_1 => refl_trans_clos (fun x y => S x y) x x_1) x y
Tactic:
. aesop
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), ?S x y ↔ refl_trans_clos R x y
Tactic:
apply inc_refl_trans_eq
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => R x x_1) x y → (fun x x_1 => ?a.S✝ x x_1) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => R x x_1) x y → (fun x x_1 => ?a.S✝ x x_1) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Tactic:
simp
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), R x y → ?a.S✝ x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), R x y → ?a.S✝ x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Tactic:
. trivial
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => S x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => S x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y
Tactic:
. simp; trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), R x y → ?a.S✝ x y
Tactic:
trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => S x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y
Tactic:
simp
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), S x y → refl_trans_clos R x y

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), S x y → refl_trans_clos R x y
Tactic:
trivial
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent fun x y => (fun x x_1 => refl_trans_clos (fun x y => S x y) x x_1) x y
Tactic:
aesop
State after:
no goals