case succ.f.a
F : PFunctor
X : Type ?u.16870
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝ i) (f✝ i)
F : PFunctor
X : Type ?u.16870
f : X → Obj F X
n : ℕ
x : M F
⊢ Agree' n x x
induction' n with _ n_ih generalizing x <;>
induction x using PFunctor.M.casesOn' <;> constructor <;> try rfl
case succ.f.a
F : PFunctor
X : Type ?u.16870
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
i✝ : B F a✝
⊢ Agree' n✝ (f✝ i✝) (f✝ i✝)
case succ.f.a
F : PFunctor
X : Type ?u.16870
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝ i) (f✝ i)
intros
no goals
case succ.f.a
F : PFunctor
X : Type ?u.16870
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
i✝ : B F a✝
⊢ Agree' n✝ (f✝ i✝) (f✝ i✝)
apply n_ih
case succ.f.a
F : PFunctor
X : Type ?u.16870
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝ i) (f✝ i)
case succ.f.a
F : PFunctor
X : Type ?u.16870
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝ i) (f✝ i)
rfl