Theorem: Free.bind_inr (CoInd/FreeMonads.lean)

State before:
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ corec (bind.automaton f) (Sum.inr x) = x
Tactic:
apply Free.eq.bisim
State after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x

State before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x
Tactic:
have : ∀ x y, x = corec (bind.automaton f) (.inr y) → eq x y := by
  apply Free.equiv.coinduction
  intro x y h₁
  conv =>
    congr
    . rfl
    . rfl
    . rw [←construct_destruct x]
    . rw [←construct_destruct y]
  have h₂ := congrArg destruct h₁
  clear h₁
  rw [destruct_corec] at h₂
  cases hy: destruct y with
  | Pure r =>
    simp only [Map, hy, bind.automaton] at h₂
    rw [h₂]
    apply equivF.Pure
    rfl
  | Free n k =>
    simp only [Map, bind.automaton, hy] at h₂
    rw [h₂]
    apply equivF.Free
    intro y
    left
    rfl
State after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
this : ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x

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

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

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

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

State before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₁ : x = corec (bind.automaton f) (Sum.inr y)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    x y
Tactic:
conv =>
  congr
  . rfl
  . rfl
  . rw [←construct_destruct x]
  . rw [←construct_destruct y]
State after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₁ : x = corec (bind.automaton f) (Sum.inr y)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))

State before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₁ : x = corec (bind.automaton f) (Sum.inr y)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))
Tactic:
have h₂ := congrArg destruct h₁
State after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₁ : x = corec (bind.automaton f) (Sum.inr y)
h₂ : destruct x = destruct (corec (bind.automaton f) (Sum.inr y))
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))

State before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₁ : x = corec (bind.automaton f) (Sum.inr y)
h₂ : destruct x = destruct (corec (bind.automaton f) (Sum.inr y))
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))
Tactic:
clear h₁
State after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = destruct (corec (bind.automaton f) (Sum.inr y))
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))

State before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = destruct (corec (bind.automaton f) (Sum.inr y))
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))
Tactic:
rw [destruct_corec] at h₂
State after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = Map (corec (bind.automaton f)) (bind.automaton f (Sum.inr y))
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))

State before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = Map (corec (bind.automaton f)) (bind.automaton f (Sum.inr y))
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))
Tactic:
cases hy: destruct y with
| Pure r =>
  simp only [Map, hy, bind.automaton] at h₂
  rw [h₂]
  apply equivF.Pure
  rfl
| Free n k =>
  simp only [Map, bind.automaton, hy] at h₂
  rw [h₂]
  apply equivF.Free
  intro y
  left
  rfl
State after:
no goals

State before:
case a.Pure
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = Map (corec (bind.automaton f)) (bind.automaton f (Sum.inr y))
r : S
hy : destruct y = Functor.Pure r
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (Functor.Pure r))
Tactic:
simp only [Map, hy, bind.automaton] at h₂
State after:
case a.Pure
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
r : S
hy : destruct y = Functor.Pure r
h₂ : destruct x = Functor.Pure r
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (Functor.Pure r))

State before:
case a.Pure
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
r : S
hy : destruct y = Functor.Pure r
h₂ : destruct x = Functor.Pure r
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (Functor.Pure r))
Tactic:
rw [h₂]
State after:
case a.Pure
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
r : S
hy : destruct y = Functor.Pure r
h₂ : destruct x = Functor.Pure r
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (Functor.Pure r)) (construct (Functor.Pure r))

State before:
case a.Pure
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
r : S
hy : destruct y = Functor.Pure r
h₂ : destruct x = Functor.Pure r
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (Functor.Pure r)) (construct (Functor.Pure r))
Tactic:
apply equivF.Pure
State after:
case a.Pure.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
r : S
hy : destruct y = Functor.Pure r
h₂ : destruct x = Functor.Pure r
⊢ r = r

State before:
case a.Pure.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
r : S
hy : destruct y = Functor.Pure r
h₂ : destruct x = Functor.Pure r
⊢ r = r
Tactic:
rfl
State after:
no goals

State before:
case a.Free
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = Map (corec (bind.automaton f)) (bind.automaton f (Sum.inr y))
n : C.A
k : Container.B C n → Free C S
hy : destruct y = Functor.Free n k
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (Functor.Free n k))
Tactic:
simp only [Map, bind.automaton, hy] at h₂
State after:
case a.Free
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (Functor.Free n k))

State before:
case a.Free
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (Functor.Free n k))
Tactic:
rw [h₂]
State after:
case a.Free
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct
      (Functor.Free n
        ((corec fun x =>
            match x with
            | Sum.inr x =>
              match destruct x with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Sum.inl x =>
              match destruct x with
              | Functor.Pure r =>
                match destruct (f r) with
                | Functor.Pure r => Functor.Pure r
                | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
              | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
          Sum.inr ∘ k)))
    (construct (Functor.Free n k))

State before:
case a.Free
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct
      (Functor.Free n
        ((corec fun x =>
            match x with
            | Sum.inr x =>
              match destruct x with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Sum.inl x =>
              match destruct x with
              | Functor.Pure r =>
                match destruct (f r) with
                | Functor.Pure r => Functor.Pure r
                | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
              | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
          Sum.inr ∘ k)))
    (construct (Functor.Free n k))
Tactic:
apply equivF.Free
State after:
case a.Free.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
⊢ ∀ (x : Container.B C n),
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
        pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
      (((corec fun x =>
            match x with
            | Sum.inr x =>
              match destruct x with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Sum.inl x =>
              match destruct x with
              | Functor.Pure r =>
                match destruct (f r) with
                | Functor.Pure r => Functor.Pure r
                | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
              | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
          Sum.inr ∘ k)
        x)
      (k x)

State before:
case a.Free.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
⊢ ∀ (x : Container.B C n),
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
        pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
      (((corec fun x =>
            match x with
            | Sum.inr x =>
              match destruct x with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Sum.inl x =>
              match destruct x with
              | Functor.Pure r =>
                match destruct (f r) with
                | Functor.Pure r => Functor.Pure r
                | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
              | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
          Sum.inr ∘ k)
        x)
      (k x)
Tactic:
intro y
State after:
case a.Free.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y✝ : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y✝ = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
y : Container.B C n
⊢ ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
      y)
    (k y)

State before:
case a.Free.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y✝ : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y✝ = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
y : Container.B C n
⊢ ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
      y)
    (k y)
Tactic:
left
State after:
case a.Free.a.h
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y✝ : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y✝ = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
y : Container.B C n
⊢ (fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
      y)
    (k y)

State before:
case a.Free.a.h
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y✝ : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y✝ = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
y : Container.B C n
⊢ (fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
      y)
    (k y)
Tactic:
rfl
State after:
no goals