Theorem: Free.eq.rfl (CoInd/FreeMonads.lean)

State before:
C : _root_.Container
R : Type u₁
⊢ ∀ (x : Free C R), eq x x
Tactic:
have : ∀ (x y:Free C R), x = y → Free.eq x y := by
  apply Free.equiv.coinduction
  intro x y h
  cases h
  conv =>
    congr
    . rfl
    . rfl
    . rw [←construct_destruct x]
    . rw [←construct_destruct x]
  cases destruct x with
  | Pure r =>
    apply equivF.Pure
    rfl
  | Free node k =>
    apply equivF.Free
    intro y
    left
    rfl
State after:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
⊢ ∀ (x : Free C R), eq x x

State before:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
⊢ ∀ (x : Free C R), eq x x
Tactic:
intro x
State after:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ eq x x

State before:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ eq x x
Tactic:
apply this
State after:
case a
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ x = x

State before:
case a
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ x = x
Tactic:
rfl
State after:
no goals

State before:
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), x = y → eq x y
Tactic:
apply Free.equiv.coinduction
State after:
case a
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), x = y → equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y

State before:
case a
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), x = y → equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y
Tactic:
intro x y h
State after:
case a
C : _root_.Container
R : Type u₁
x y : Free C R
h : x = y
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y

State before:
case a
C : _root_.Container
R : Type u₁
x y : Free C R
h : x = y
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y
Tactic:
cases h
State after:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x x

State before:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x x
Tactic:
conv =>
  congr
  . rfl
  . rfl
  . rw [←construct_destruct x]
  . rw [←construct_destruct x]
State after:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (destruct x)) (construct (destruct x))

State before:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (destruct x)) (construct (destruct x))
Tactic:
cases destruct x with
| Pure r =>
  apply equivF.Pure
  rfl
| Free node k =>
  apply equivF.Free
  intro y
  left
  rfl
State after:
no goals

State before:
case a.refl.Pure
C : _root_.Container
R : Type u₁
x : Free C R
r : R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (Functor.Pure r)) (construct (Functor.Pure r))
Tactic:
apply equivF.Pure
State after:
case a.refl.Pure.a
C : _root_.Container
R : Type u₁
x : Free C R
r : R
⊢ r = r

State before:
case a.refl.Pure.a
C : _root_.Container
R : Type u₁
x : Free C R
r : R
⊢ r = r
Tactic:
rfl
State after:
no goals

State before:
case a.refl.Free
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (Functor.Free node k))
    (construct (Functor.Free node k))
Tactic:
apply equivF.Free
State after:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
⊢ ∀ (x : Container.B C node), ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k x) (k x)

State before:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
⊢ ∀ (x : Container.B C node), ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k x) (k x)
Tactic:
intro y
State after:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k y) (k y)

State before:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k y) (k y)
Tactic:
left
State after:
case a.refl.Free.a.h
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ (fun x y => x = y) (k y) (k y)

State before:
case a.refl.Free.a.h
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ (fun x y => x = y) (k y) (k y)
Tactic:
rfl
State after:
no goals