Theorem: QPF.M.map_comp (CoInd/QPF/M.lean)

State before:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> x = f <$> g <$> x
Tactic:
conv =>
  congr
  <;> rw [←inst.abs_repr x]
State after:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> abs (repr x) = f <$> g <$> abs (repr x)

State before:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> abs (repr x) = f <$> g <$> abs (repr x)
Tactic:
cases repr x
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ (f ∘ g) <$> abs { fst := fst✝, snd := snd✝ } = f <$> g <$> abs { fst := fst✝, snd := snd✝ }

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ (f ∘ g) <$> abs { fst := fst✝, snd := snd✝ } = f <$> g <$> abs { fst := fst✝, snd := snd✝ }
Tactic:
simp [←inst.abs_map, Container.Map]
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ abs { fst := fst✝, snd := (f ∘ g) ∘ snd✝ } = abs { fst := fst✝, snd := f ∘ g ∘ snd✝ }

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ abs { fst := fst✝, snd := (f ∘ g) ∘ snd✝ } = abs { fst := fst✝, snd := f ∘ g ∘ snd✝ }
Tactic:
rfl
State after:
no goals