awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation (F := F)
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' :
  Eq (α := F α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
    (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f'))
i : Fin2 n
mp :
  supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)
      i =
    f' i '' univ
mp₁ :
  Eq.{u + 1} (α := Set (α i))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) i)
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
mp₂ :
  Eq (α := Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i)
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
mp₃ :
  Eq (α := Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f')) i)
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
⊢ f i '' univ = f' i '' univ
have mp₄ : Eq.{u + 1} (α := Set (α i))
  (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
  (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
Tactic: rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform (F := F)
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ Eq (α := (i : Fin2 n) → Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
have mpr : ∀ (x : Fin2 n) (x_1 : α x),
  Membership.mem (γ := Set (α x))
      (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) x_1 ↔
    Membership.mem (γ := Set (α x))
      (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform (F := F)
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x : Fin2 n
x_1 : α x
⊢ Membership.mem (γ := Set (α x))
      (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) x_1 ↔
    Membership.mem (γ := Set (α x))
      (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
      x_1
have mpr : x_1 ∈ f x '' univ ↔
  Membership.mem (γ := Set (α x))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
    x_1
Tactic: rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform (F := F)
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x : Fin2 n
x_1 : α x
mpr :
  x_1 ∈ f x '' univ ↔
    Membership.mem (γ := Set (α x))
      (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
      x_1
mpr₁ : IsUniform (F := F)
⊢ Membership.mem (γ := Set (α x))
      (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) x_1 ↔
    Membership.mem (γ := Set (α x))
      (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
      x_1
have mpr₂ : x_1 ∈ f x '' univ ↔ x_1 ∈ f x '' univ
Tactic: rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation (F := F) ↔ LiftPPreservation (F := F)
have mp : SuppPreservation (F := F) → LiftPPreservation (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
mp : SuppPreservation (F := F) → LiftPPreservation (F := F)
⊢ SuppPreservation (F := F) ↔ LiftPPreservation (F := F)
have mpr : LiftPPreservation (F := F) → SuppPreservation (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (hypothesis)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation (F := F)
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : SuppPreservation (F := F)
⊢ LiftP (F := F) (α := α) p (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) ↔
    LiftP (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) p
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)
have h'₁ : IsUniform (F := F)
Tactic: rw [suppPreservation_iff_isUniform] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
⊢ LiftP (F := F) (α := α) p (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) ↔
    LiftP (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) p
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)
have mp : (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
Tactic: simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h',
      image_univ, mem_range, exists_imp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
have mp : (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) → ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
mp : (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) → ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
have mp₁ : (∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)) → ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
h_1 : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i : Fin2 n
u : α i
x : (P F).B a i
h_2 : f i x = u
⊢ p u
have mp : p (f i x)
Tactic: subst_vars
Cleared hypotheses: u, h_2
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    LiftP (F := F) (α := α) p (abs (F := F) (α := α) x) ↔
      LiftP (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) p x
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ Eq (α := (i : Fin2 n) → Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
have mpr : ∀ (x : Fin2 n) (x_1 : α x),
  Membership.mem (γ := Set (α x))
      (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) x_1 ↔
    Membership.mem (γ := Set (α x))
      (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ LiftPPreservation (F := F) ↔ IsUniform (F := F)
have rw : SuppPreservation (F := F) ↔ IsUniform (F := F)
Tactic: rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
rw : SuppPreservation (F := F) ↔ IsUniform (F := F)
⊢ LiftPPreservation (F := F) ↔ IsUniform (F := F)
have rw₁ : IsUniform (F := F) ↔ IsUniform (F := F)
Tactic: rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ M.dest (P F) (α := α) (corecF (F := F) (α := α) g x) =
    MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corecF (F := F) (α := α) g))
      (repr (F := F) (α := α ::: β) (g x))
have rw : M.dest (P F) (α := α) (M.corec (P F) (α := α) (fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)) x) =
  MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (M.corec (P F) (α := α) fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)))
    (repr (F := F) (α := α ::: β) (g x))
Tactic: rw [corecF, M.dest_corec]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
rw :
  M.dest (P F) (α := α) (M.corec (P F) (α := α) (fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)) x) =
    MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α) fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)))
      (repr (F := F) (α := α ::: β) (g x))
⊢ M.dest (P F) (α := α) (corecF (F := F) (α := α) g x) =
    MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corecF (F := F) (α := α) g))
      (repr (F := F) (α := α ::: β) (g x))
have rw₁ : Eq (α := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: (P F).M α))
  (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (M.corec (P F) (α := α) fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)))
    (repr (F := F) (α := α ::: β) (g x)))
  (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (M.corec (P F) (α := α) fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)))
    (repr (F := F) (α := α ::: β) (g x)))
Tactic: rw [corecF, M.dest_corec]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
⊢ Eq.{u + 1} (α := Cofix F β)
    ((fun (x : (P F).M α) ↦
        (Quot.mk (Mcongr (F := F) (α := β)) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) :
          Quot (α := (P F).M β) (Mcongr (F := F) (α := β))))
      aa₁)
    ((fun (x : (P F).M α) ↦
        (Quot.mk (Mcongr (F := F) (α := β)) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) :
          Quot (α := (P F).M β) (Mcongr (F := F) (α := β))))
      aa₂)
have a : Mcongr (F := F) (α := β) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁)
  (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
⊢ Mcongr (F := F) (α := β) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁)
    (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
have h : IsPrecongr (F := F) (α := β) r' ∧
  r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
Tactic: use r'
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
⊢ IsPrecongr (F := F) (α := β) r' ∧
    r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
have h : IsPrecongr (F := F) (α := β) r'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
h : IsPrecongr (F := F) (α := β) r'
⊢ IsPrecongr (F := F) (α := β) r' ∧
    r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
have h₁ : r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁_1 a₂_1 : (P F).M α
ra₁a₂_2 : r a₁_1 a₂_1
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁_1
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂_1
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
⊢ Eq.{u + 1} (α := Quot r') ((fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) a₁)
    ((fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) a₂)
have a : r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂)
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
⊢ (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
have h : ∀ (x : (P F).M α),
  (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) x = (u ∘ Quot.mk r) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (hypothesis)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
⊢ abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := β ::: (P F).M β) (β := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r')) (M.dest (P F) (α := β) b₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := β ::: (P F).M β) (β := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r')) (M.dest (P F) (α := β) b₂))
have hu : (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
Tactic: have hu : (Quot.mk r' ∘ fun x : q.P.M α => g <$$> x) = u ∘ Quot.mk r := by
          ext x
          rfl
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
hu : (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
⊢ abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := β ::: (P F).M β) (β := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r')) (M.dest (P F) (α := β) b₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := β ::: (P F).M β) (β := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r')) (M.dest (P F) (α := β) b₂))
have h : abs (F := F) (α := β ::: Quot r')
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
      (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
        (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
      (M.dest (P F) (α := α) a₁)) =
  abs (F := F) (α := β ::: Quot r')
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
      (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
        (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
      (M.dest (P F) (α := α) a₂))
Tactic: rw [b₁eq, b₂eq, M.dest_map, M.dest_map, ← q.P.comp_map, ← q.P.comp_map]