Theorem: normalizes_trans (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ normalizing R → normalizing fun x x_1 => trans_clos R x x_1
Tactic:
intros norm
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ normalizing fun x x_1 => trans_clos R x x_1

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ normalizing fun x x_1 => trans_clos R x x_1
Tactic:
apply ind_normalizing
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x) → ∀ (x : A), P x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x) → ∀ (x : A), P x
Tactic:
intros P ih
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
⊢ ∀ (x : A), P x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
⊢ ∀ (x : A), P x
Tactic:
let Q := λ x ↦ P x ∧ ∀ y, x ~>+ y → P y
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
⊢ ∀ (x : A), P x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
⊢ ∀ (x : A), P x
Tactic:
have h : ∀ x, Q x :=
by
  intros x
  apply normalizing_ind R
  . intros x ih'
    constructor
    . apply ih
      intros y red_x_y
      cases red_x_y
      . apply (ih' _ _).1; trivial
      . apply (ih' _ _).2 <;> trivial
    . intros y red_x_y
      cases red_x_y
      . apply (ih' _ _).1; trivial
      . apply (ih' _ _).2 <;> trivial
  . trivial
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
⊢ ∀ (x : A), P x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
⊢ ∀ (x : A), P x
Tactic:
intros x
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
x : A
⊢ P x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
x : A
⊢ P x
Tactic:
apply (h x).1
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
⊢ ∀ (x : A), Q x
Tactic:
intros x
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ Q x

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ Q x
Tactic:
apply normalizing_ind R
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → Q y) → Q x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → Q y) → Q x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Tactic:
. intros x ih'
  constructor
  . apply ih
    intros y red_x_y
    cases red_x_y
    . apply (ih' _ _).1; trivial
    . apply (ih' _ _).2 <;> trivial
  . intros y red_x_y
    cases red_x_y
    . apply (ih' _ _).1; trivial
    . apply (ih' _ _).2 <;> trivial
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Tactic:
. trivial
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → Q y) → Q x
Tactic:
intros x ih'
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ Q x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ Q x
Tactic:
constructor
State after:
case a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ P x

case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y

State before:
case a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ P x

case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
. apply ih
  intros y red_x_y
  cases red_x_y
  . apply (ih' _ _).1; trivial
  . apply (ih' _ _).2 <;> trivial
State after:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y

State before:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
. intros y red_x_y
  cases red_x_y
  . apply (ih' _ _).1; trivial
  . apply (ih' _ _).2 <;> trivial
State after:
no goals

State before:
case a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ P x
Tactic:
apply ih
State after:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y

State before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
intros y red_x_y
State after:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y

State before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y
Tactic:
cases red_x_y
State after:
case a.left.a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y

State before:
case a.left.a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).1; trivial
State after:
case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y

State before:
case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).2 <;> trivial
State after:
no goals

State before:
case a.left.a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y
Tactic:
apply (ih' _ _).1
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ R x y
Tactic:
trivial
State after:
no goals

State before:
case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
apply (ih' _ _).2 <;> trivial
State after:
no goals

State before:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
intros y red_x_y
State after:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y

State before:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y
Tactic:
cases red_x_y
State after:
case a.right.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y

State before:
case a.right.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).1; trivial
State after:
case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y

State before:
case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).2 <;> trivial
State after:
no goals

State before:
case a.right.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y
Tactic:
apply (ih' _ _).1
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ R x y

State before:
case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
apply (ih' _ _).2 <;> trivial
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Tactic:
trivial
State after:
no goals