Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ M.mk ⟨a✝, f✝¹⟩ = M.mk ⟨?mp.succ.f.f.intro.a✝, ?mp.succ.f.f.intro.x⟩

pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?mp.succ.f.f.intro.a✝, ?mp.succ.f.f.intro.y⟩

pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B ?mp.succ.f.f.intro.a✝), Agree' n✝ (?mp.succ.f.f.intro.x i) (?mp.succ.f.f.intro.y i)

pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ F.A

pp: case mp.succ.f.f.intro.x
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ F.B ?mp.succ.f.f.intro.a✝ → F.M

pp: case mp.succ.f.f.intro.y
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ F.B ?mp.succ.f.f.intro.a✝ → F.M

Tactic:
<;>

Goal state after:
case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ M.mk ⟨a✝, f✝¹⟩ = M.mk ⟨?mp.succ.f.f.intro.a✝, ?mp.succ.f.f.intro.x⟩

case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?mp.succ.f.f.intro.a✝, ?mp.succ.f.f.intro.y⟩

case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B ?mp.succ.f.f.intro.a✝), Agree' n✝ (?mp.succ.f.f.intro.x i) (?mp.succ.f.f.intro.y i)

case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ F.A

case mp.succ.f.f.intro.x
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ F.B ?mp.succ.f.f.intro.a✝ → F.M

case mp.succ.f.f.intro.y
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ F.B ?mp.succ.f.f.intro.a✝ → F.M