awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h :
  Eq (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
    (abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))
⊢ Eq (α := F (β ::: (P F).W β))
    (abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (x : (P F).last.B a₀) ↦
        (P F).wMap (α := α) (β := β) g (f₀ x)))
    (abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x)))
have abs : abs (F := F) (α := β ::: (P F).W β)
    (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
  abs (F := F) (α := β ::: (P F).W β)
    ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
      (P F).wMap (α := α) (β := β) g (f₁ x))
Tactic: rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h :
  Eq (α := F (α ::: (P F).W α))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))
abs :
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x))
⊢ Eq (α := F (β ::: (P F).W β))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (x : (P F).last.B a₀) ↦
        (P F).wMap (α := α) (β := β) g (f₀ x)))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x)))
have abs₁ : MvQPF.abs (F := F) (α := β ::: (P F).W β)
    (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
    (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
Tactic: rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h :
  Eq (α := F (α ::: (P F).W α))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))
abs :
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x))
abs₁ :
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
⊢ Eq (α := F (β ::: (P F).W β))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (x : (P F).last.B a₀) ↦
        (P F).wMap (α := α) (β := β) g (f₀ x)))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x)))
have abs₂ : map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
    (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
    (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
Tactic: rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h :
  Eq (α := F (α ::: (P F).W α))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))
abs :
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x))
abs₁ :
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
abs₂ :
  map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
      (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
⊢ Eq (α := F (β ::: (P F).W β))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (x : (P F).last.B a₀) ↦
        (P F).wMap (α := α) (β := β) g (f₀ x)))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x)))
have abs₃ : map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
    (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
  map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
    (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
Tactic: rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x_1 y_1 x y z : (P F).W α
h : WEquiv (F := F) (α := α) x y
h_1 : WEquiv (F := F) (α := α) y z
ih₁ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
ih₂ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y) (map (F := (P F).W) (α := α) (β := β) g z)
trans : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
trans₁ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y) (map (F := (P F).W) (α := α) (β := β) g z)
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g z)
have trans₂ : (P F).W β
Tactic: apply MvQPF.WEquiv.trans
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv (F := F) (α := α) x y
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
have ind : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α)
  (h : ∀ (x : (P F).last.B a), WEquiv (F := F) (α := α) (f₀ x) (f₁ x))
  (ih :
    ∀ (x : (P F).last.B a),
      WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g (f₀ x))
        (map (F := (P F).W) (α := α) (β := β) g (f₁ x))),
  WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₀))
    (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₁))
Tactic: induction h with
  | ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
    rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
    change
      abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
        abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
    rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
  | trans x y z _ _ ih₁ ih₂ =>
    apply MvQPF.WEquiv.trans
    · apply ih₁
    · apply ih₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv (F := F) (α := α) x y
ind :
  ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α)
    (h : ∀ (x : (P F).last.B a), WEquiv (F := F) (α := α) (f₀ x) (f₁ x))
    (ih :
      ∀ (x : (P F).last.B a),
        WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g (f₀ x))
          (map (F := (P F).W) (α := α) (β := β) g (f₁ x))),
    WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₀))
      (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₁))
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
have abs : ∀ (a₀ : (P F).A) (f'₀ : (P F).drop.B a₀ ⟹ α) (f₀ : (P F).last.B a₀ → (P F).W α) (a₁ : (P F).A)
  (f'₁ : (P F).drop.B a₁ ⟹ α) (f₁ : (P F).last.B a₁ → (P F).W α)
  (h :
    Eq (α := F (α ::: (P F).W α))
      (abs (F := F) (α := α ::: (P F).W α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
      (abs (F := F) (α := α ::: (P F).W α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))),
  WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a₀ f'₀ f₀))
    (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a₁ f'₁ f₁))
Tactic: induction h with
  | ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
    rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
    change
      abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
        abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
    rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
  | trans x y z _ _ ih₁ ih₂ =>
    apply MvQPF.WEquiv.trans
    · apply ih₁
    · apply ih₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv (F := F) (α := α) x y
ind :
  ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α)
    (h : ∀ (x : (P F).last.B a), WEquiv (F := F) (α := α) (f₀ x) (f₁ x))
    (ih :
      ∀ (x : (P F).last.B a),
        WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g (f₀ x))
          (map (F := (P F).W) (α := α) (β := β) g (f₁ x))),
    WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₀))
      (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₁))
abs :
  ∀ (a₀ : (P F).A) (f'₀ : (P F).drop.B a₀ ⟹ α) (f₀ : (P F).last.B a₀ → (P F).W α) (a₁ : (P F).A)
    (f'₁ : (P F).drop.B a₁ ⟹ α) (f₁ : (P F).last.B a₁ → (P F).W α)
    (h :
      Eq (α := F (α ::: (P F).W α))
        (MvQPF.abs (F := F) (α := α ::: (P F).W α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
        (MvQPF.abs (F := F) (α := α ::: (P F).W α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))),
    WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a₀ f'₀ f₀))
      (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a₁ f'₁ f₁))
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
have trans : ∀ (x y z : (P F).W α),
  WEquiv (F := F) (α := α) x y →
    WEquiv (F := F) (α := α) y z →
      ∀
        (ih₁ :
          WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x)
            (map (F := (P F).W) (α := α) (β := β) g y))
        (ih₂ :
          WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y)
            (map (F := (P F).W) (α := α) (β := β) g z)),
        WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g z)
Tactic: induction h with
  | ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
    rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
    change
      abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
        abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
    rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
  | trans x y z _ _ ih₁ ih₂ =>
    apply MvQPF.WEquiv.trans
    · apply ih₁
    · apply ih₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
have h : ∀ (x : Fix F α), (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) x = rec (F := F) (α := α) g x
Tactic: apply funext
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (x : Fix F α), (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) x = rec (F := F) (α := α) g x
have h : ∀ (a : (P F).W α), (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) ⟦a⟧ = rec (F := F) (α := α) g ⟦a⟧
Tactic: apply Quotient.ind
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x_1 : F (α ::: Fix F α)
x : (P F).W α
⊢ (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) ⟦x⟧ = rec (F := F) (α := α) g ⟦x⟧
have h : WEquiv (F := F) (α := α) (fixToW (F := F) (α := α) ⟦x⟧) x
Tactic: apply recF_eq_of_wEquiv
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (hypothesis)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
have this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
Tactic: have : recF g ∘ fixToW = Fix.rec g := by
    apply funext
    apply Quotient.ind
    intro x
    apply recF_eq_of_wEquiv
    apply wrepr_equiv
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
| rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
have lhs : rec (F := F) (α := α) g (mk (F := F) (α := α) x)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
| rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
have rw : recF (F := F) (α := α) g
  ((P F).wMk' (α := α)
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
      (repr (F := F) (α := α ::: Fix F α) x)))
Tactic: lhs
    rw [Fix.rec, Fix.mk]
    dsimp
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
⊢ recF (F := F) (α := α) g
      ((P F).wMk' (α := α)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          (repr (F := F) (α := α ::: Fix F α) x))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
have rcases : ∀ (a : (P F).A) (f : (P F).B a ⟹ α ::: Fix F α)
  (h : repr (F := F) (α := α ::: Fix F α) x = Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f),
  recF (F := F) (α := α) g
      ((P F).wMk' (α := α)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
Tactic: rcases h : repr x with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr (F := F) (α := α ::: Fix F α) x = Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f
⊢ recF (F := F) (α := α) g
      ((P F).wMk' (α := α)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
have rw : g
    (abs (F := F) (α := α ::: β)
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f)))) =
  g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
Tactic: rw [MvPFunctor.map_eq, recF_eq', ← MvPFunctor.map_eq, MvPFunctor.wDest'_wMk']