Theorem: Free.equiv.coinduction (CoInd/FreeMonads.lean)

State before:
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
⊢ (∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y) →
    ∀ (x : Free C R) (y : Free C S), P x y → equiv eq x y
Tactic:
intro h x y h'
State after:
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ equiv eq x y

State before:
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ equiv eq x y
Tactic:
apply (pgfp.coinduction (equivF' eq) P).2
State after:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P ≤ ↑(equivF' eq) (P ⊔ ↑(pgfp (equivF' eq)) P)

case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y

State before:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P ≤ ↑(equivF' eq) (P ⊔ ↑(pgfp (equivF' eq)) P)

case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y
Tactic:
apply h
State after:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y

State before:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y
Tactic:
apply h'
State after:
no goals