internlm/Lean-Github huggingface dataset:
Theorem: Free.bind_inr
Proof 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₁
Proof 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
Theorem: Free.bind_inr
Proof 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]
Proof 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))
Theorem: Free.bind_inr
Proof 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₁
Proof 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))
Theorem: Free.bind_inr
Proof 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₁
Proof 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))
Theorem: Free.bind_inr
Proof 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₂
Proof 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))
Theorem: Free.bind_inr
Proof 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
Proof state after:
no goals
Theorem: Free.bind_inr
Proof 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₂
Proof 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))
Theorem: Free.bind_inr
Proof 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₂]
Proof 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))
Theorem: Free.bind_inr
Proof 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
Proof 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
Theorem: Free.bind_inr
Proof 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
Proof state after:
no goals
Theorem: Free.bind_inr
Proof 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₂
Proof 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))
Theorem: Free.bind_inr
Proof 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₂]
Proof 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))
Theorem: Free.bind_inr
Proof 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
Proof 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)
Theorem: Free.bind_inr
Proof 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
Proof 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)
Theorem: Free.bind_inr
Proof 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
Proof 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)
Theorem: Free.bind_inr
Proof 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
Proof state after:
no goals
Theorem: Free.bind_pure
Proof state before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ bind (pure r) k = k r
Tactic:
rw [←construct_destruct <| k r]
Proof state after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ bind (pure r) k = construct (destruct (k r))
Theorem: Free.bind_pure
Proof state before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ bind (pure r) k = construct (destruct (k r))
Tactic:
rw [←construct_destruct <| bind (pure r) k]
Proof state after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (destruct (bind (pure r) k)) = construct (destruct (k r))
Theorem: Free.bind_pure
Proof state before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (destruct (bind (pure r) k)) = construct (destruct (k r))
Tactic:
simp only [bind, pure, destruct_corec]
Proof state after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r))))) =
    construct (destruct (k r))
Theorem: Free.bind_pure
Proof state before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r))))) =
    construct (destruct (k r))
Tactic:
apply congrArg construct
Proof state after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r)))) = destruct (k r)
Theorem: Free.bind_pure
Proof state before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r)))) = destruct (k r)
Tactic:
conv =>
  lhs
  congr
  . rfl
  . simp only [bind.automaton, destruct_construct]
Proof state after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (Map Sum.inr (destruct (k r))) = destruct (k r)
Theorem: Free.bind_pure
Proof state before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (Map Sum.inr (destruct (k r))) = destruct (k r)
Tactic:
cases destruct (k r) with
| Pure r =>
  simp only [Map]
| Free n k =>
  simp only [Map]
  conv =>
    lhs
    congr
    simp only [Function.comp]
    intro x
    rw [bind_inr]
Proof state after:
no goals
Theorem: Free.bind_pure
Proof state before:
case Pure
C : _root_.Container
R S : Type u₁
r✝ : R
k : R → Free C S
r : S
⊢ Map (corec (bind.automaton k)) (Map Sum.inr (Functor.Pure r)) = Functor.Pure r
Tactic:
simp only [Map]
Proof state after:
no goals