awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
⊢ ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
      y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
have mp : ∀ (a : P.A) (f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
  (h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f),
  ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
      y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
Tactic: rcases h : u with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
      y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
have h₁ : (x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1) ∧
  (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : P.B a i),
      r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) i j)
Tactic: use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ (x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1) ∧
    (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
      ∀ (i : Fin2 n) (j : P.B a i),
        r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) i j)
have h₁ : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1
⊢ (x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1) ∧
    (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
      ∀ (i : Fin2 n) (j : P.B a i),
        r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) i j)
have h₂ : (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
  ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1
have h₁ : Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
  (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
    (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1)
Tactic: rw [← xeq, h]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
have h₁ : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2
⊢ (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
have h₂ : ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2
have h₁ : Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
  (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
    (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2)
Tactic: rw [← yeq, h]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
⊢ supp (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) i =
    f i '' univ
have h : ∀ (x : α i),
  Membership.mem (γ := Set (α i))
      (supp (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) i) x ↔
    x ∈ f i '' univ
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ Membership.mem (γ := Set (α i))
      (supp (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) i) x ↔
    x ∈ f i '' univ
have h : (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x) ↔
  ∃ (y : P.B a i), f i y = x
Tactic: simp only [supp, image_univ, mem_range, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
      LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
        P_1 i x) ↔
    ∃ (y : P.B a i), f i y = x
have h : (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x) →
  ∃ (y : P.B a i), f i y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
      LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
        P_1 i x) →
    ∃ (y : P.B a i), f i y = x
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
      LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
        P_1 i x) ↔
    ∃ (y : P.B a i), f i y = x
have h₁ : (∃ (y : P.B a i), f i y = x) →
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
⊢ ∃ (y : P.B a i), f i y = x
have h₁ : LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (fun (i : Fin2 n) (x : α i) ↦ ∃ (y : P.B a i), f i y = x)
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
Tactic: apply @h fun i x => ∃ y : P.B a i, f i y = x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (fun (i : Fin2 n) (x : α i) ↦ ∃ (y : P.B a i), f i y = x)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
have h₁ : ∀ (i : Fin2 n) (x : P.B a i), ∃ (y : P.B a i), f i y = f i x
Tactic: rw [liftP_iff']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ (y : P.B a i), f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
have h₁ : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x
Tactic: simp only [liftP_iff']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ (y : P.B a i), f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x
have h₁ : ∀ (w : P.B a i),
  f i w = x → ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
w : P.B a i
h : f i w = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x
have h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i (f i w)
Tactic: subst x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
have rw : ∀
  (h' :
    Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
      (PFunctor.map.{u, u, v, u} P.last (α := β)
        (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
        (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f))
  (c : P.drop.B a i) (h : x = corecShape P g₀ g₂ b), a = g₀ b
Tactic: rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
Cleared hypotheses: h', c, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' :
  Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
    (PFunctor.map.{u, u, v, u} P.last (α := β)
      (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
    (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
have refl : ∀ (c : P.drop.B (g₀ b) i), g₀ b = g₀ b
Tactic: cases h'
Cleared hypotheses: a, f, h', c
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
have rw : ∀
  (h' :
    Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
      (PFunctor.map.{u, u, v, u} P.last (α := β)
        (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
        (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f))
  (j : P.last.B a) (c : Path P (f j) i) (h : x = corecShape P g₀ g₂ b), a = g₀ b
Tactic: rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
Cleared hypotheses: h', j, c, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' :
  Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
    (PFunctor.map.{u, u, v, u} P.last (α := β)
      (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
    (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
have refl : ∀ (j : P.last.B (g₀ b))
  (c :
    Path P
      (((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j)
      i),
  g₀ b = g₀ b
Tactic: cases h'
Cleared hypotheses: a, f, h', j, c
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
have rw : ∀
  (h' :
    Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
      (PFunctor.map.{u, u, v, u} P.last (α := β)
        (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
        (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f))
  (j : P.last.B a) (c : Path P (f j) i) (h : x = corecShape P g₀ g₂ b) (h₀ : a = g₀ b),
  f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
Tactic: rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
Cleared hypotheses: h', j, c, h, h₀
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' :
  Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
    (PFunctor.map.{u, u, v, u} P.last (α := β)
      (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
    (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
have refl : ∀ (j : P.last.B (g₀ b)) (h₀ : g₀ b = g₀ b)
  (c :
    Path P
      (((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j)
      i),
  ((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j =
    corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
Tactic: cases h'
Cleared hypotheses: a, f, h', j, c, h₀
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a₁ : P.A
f₁ : P.last.B a₁ → P.last.M
h₁ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁ f₁
a₂ : P.A
f₂ : P.last.B a₂ → P.last.M
h₂ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₂ f₂
f' : Path P x ⟹ α
⊢ dest' P (α := α) h₁ f' = dest' P (α := α) h₂ f'
have refl : ∀ (h₂ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁ f₁),
  dest' P (α := α) h₁ f' = dest' P (α := α) h₂ f'
Tactic: cases h₁.symm.trans h₂
Cleared hypotheses: a₂, f₂, h₂