awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 →
    (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
      x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
mpr₅ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.2 ≤ y.2
mpr₆ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → ¬y.2 ≤ x.2
mp₉ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁₀ mp₁₁ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2
mp₁₃ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → ¬y.2 ≤ x.2
mpr₇ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.1 → y.1 ≤ x.1
mpr₈ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₉ : x.1 ≤ y.1 → ¬x.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → y.1 ≤ x.1
mpr₁₀ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → y.1 ≤ x.1
mpr₁₁ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₂ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → y.1 ≤ x.1
mpr₁₃ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₄ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → y.1 ≤ x.1
mpr₁₅ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.1 → x.2 ≤ y.2
mpr₁₆ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁₇ : x.1 ≤ y.1 → ¬x.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.2 ≤ y.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mpr₁₈ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.2 ≤ y.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β))
have inl : ∀ (h : (a₁, b₁) < (a₁, b₂)),
  LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₂) : Lex (α × β))
Tactic: obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
Cleared hypotheses: a₂, h
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
inl :
  ∀ (h : (a₁, b₁) < (a₁, b₂)),
    LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₂) : Lex (α × β))
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β))
have inr : ∀ (ha : (a₁, b₁).1 < (a₂, b₂).1),
  LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β))
Tactic: obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
⊢ compare a b = compareOfLessAndEq a b
have have : ∀ (this : DecidableLT (Lex (α × β))), compare a b = compareOfLessAndEq a b
Tactic: have : DecidableLT (α ×ₗ β) := Prod.Lex.decidable _ _
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (hypothesis)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this : DecidableLT (Lex (α × β))
⊢ compare a b = compareOfLessAndEq a b
have this₁ : Std.LawfulBEqOrd (Lex (α × β))
Tactic: have : Std.LawfulBEqOrd (α ×ₗ β) := ⟨by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]⟩
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (hypothesis)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this_1 : DecidableLT (Lex (α × β))
this : Std.LawfulBEqOrd (Lex (α × β))
⊢ compare a b = compareOfLessAndEq a b
have this₁ : Std.LawfulLTOrd (Lex (α × β))
Tactic: have : Std.LawfulLTOrd (α ×ₗ β) := ⟨by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_lt, toLex_lt_toLex,
        compare_lt_iff_lt]⟩
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
⊢ ∃ (a : Lex (α × β)), (a₁, b₁) < a ∧ a < (a₂, b₂)
have left : ∀ (c : α) (h₁ : a₁ < c) (h₂ : c < a₂), ∃ (a : Lex (α × β)), (a₁, b₁) < a ∧ a < (a₂, b₂)
Tactic: obtain ⟨c, h₁, h₂⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
⊢ ∃ (a_1 : Lex (α × β)), (a, b₁) < a_1 ∧ a_1 < (a, b₂)
have right : ∀ (c : β) (h₁ : b₁ < c) (h₂ : c < b₂), ∃ (a_1 : Lex (α × β)), (a, b₁) < a_1 ∧ a_1 < (a, b₂)
Tactic: obtain ⟨c, h₁, h₂⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder α
⊢ ∀ (a : Lex (α × β)), ∃ (b : Lex (α × β)), a < b
have rw : ∀ (a : α) (b : β), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
Tactic: rw [Lex.forall, Prod.forall]
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder α
a : α
b : β
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
have obtain : ∀ (c : α) (h : a < c), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
Tactic: obtain ⟨c, h⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder α
a : α
b : β
c : α
h : a < c
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
have h₁ : LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))
  ((toLex : (a : α × β) → Lex (α × β)) (c, b) : Lex (α × β))
Tactic: use toLex (c, b)
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder β
⊢ ∀ (a : Lex (α × β)), ∃ (b : Lex (α × β)), a < b
have rw : ∀ (a : α) (b : β), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
Tactic: rw [Lex.forall, Prod.forall]
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder β
a : α
b : β
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
have obtain : ∀ (c : β) (h : b < c), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
Tactic: obtain ⟨c, h⟩ := exists_gt b
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder β
a : α
b c : β
h : b < c
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
have h₁ : LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))
  ((toLex : (a : α × β) → Lex (α × β)) (a, c) : Lex (α × β))
Tactic: use toLex (a, c)
-- Lean 4 proof step from Mathlib.Data.Prod.PProd (goal)
Goal:
α_1 : Sort u_1
β_1 : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
x₂ : α
y₂ : β
h : (x₁, y₁) = (x₂, y₂)
P : Sort u_7
w : x₁ = x₂ → y₁ = y₂ → P
⊢ P
have refl : (w : x₁ = x₁ → y₁ = y₁ → P) → P
Tactic: cases h
Cleared hypotheses: x₂, y₂, h, w
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i_1 j_1 : ι
l : List ι
inst : DecidableEq ι
i : ι
is : List ι
v : TProd α (i :: is)
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ α j
have subst : (v : TProd α (j :: is)) → (hj : j ∈ j :: is) → α j
Tactic: subst hji
Cleared hypotheses: i, v, hj, hji
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst : DecidableEq ι
hl : (i :: l).Nodup
hj : j ∈ l
v : TProd α (i :: l)
⊢ v.elim (α := α) ⋯ = TProd.elim (α := α) v.2 hj
have hji : j ≠ i
Tactic: apply elim_of_ne
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
have pos : ∀ (hji : j = i), (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
pos : ∀ (hji : j = i), (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
have neg : ∀ (hji : ¬j = i), (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
have pos : ∀ (hj : j ∈ j :: is), (TProd.mk (α := α) (j :: is) f).elim (α := α) hj = f j
Tactic: subst hji
Cleared hypotheses: i, hj, hji
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
have neg : TProd.elim (α := α) (TProd.mk (α := α) (i :: is) f).2 sorry = f j
Tactic: rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
neg : TProd.elim (α := α) (TProd.mk (α := α) (i :: is) f).2 ⋯ = f j
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
have neg₁ : (TProd.mk (α := α) is f).elim (α := α) sorry = f j
Tactic: rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
neg : TProd.elim (α := α) (TProd.mk (α := α) (i :: is) f).2 ⋯ = f j
neg₁ : (TProd.mk (α := α) is f).elim (α := α) ⋯ = f j
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
have neg₂ : f j = f j
Tactic: rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
⊢ v = w
have fst : v.1 = w.1
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
fst : v.1 = w.1
⊢ v = w
have snd : v.2 = w.2
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
⊢ v.1 = w.1
have fst : v.elim (α := α) sorry = w.1
Tactic: rw [← elim_self v, hvw, elim_self]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
fst : v.elim (α := α) ⋯ = w.1
⊢ v.1 = w.1
have fst₁ : w.elim (α := α) sorry = w.1
Tactic: rw [← elim_self v, hvw, elim_self]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
fst : v.elim (α := α) ⋯ = w.1
fst₁ : w.elim (α := α) ⋯ = w.1
⊢ v.1 = w.1
have fst₂ : w.1 = w.1
Tactic: rw [← elim_self v, hvw, elim_self]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
⊢ v.2 = w.2
have snd : ∀ (j : ι) (hj : j ∈ is), TProd.elim (α := α) v.2 hj = TProd.elim (α := α) w.2 hj
Tactic: refine ext (nodup_cons.mp hl).2 fun j hj => ?_
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
j : ι
hj : j ∈ is
⊢ TProd.elim (α := α) v.2 hj = TProd.elim (α := α) w.2 hj
have snd : v.elim (α := α) sorry = TProd.elim (α := α) w.2 hj
Tactic: rw [← elim_of_mem hl, hvw, elim_of_mem hl]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
j : ι
hj : j ∈ is
snd : v.elim (α := α) ⋯ = TProd.elim (α := α) w.2 hj
⊢ TProd.elim (α := α) v.2 hj = TProd.elim (α := α) w.2 hj
have snd₁ : w.elim (α := α) sorry = TProd.elim (α := α) w.2 hj
Tactic: rw [← elim_of_mem hl, hvw, elim_of_mem hl]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
j : ι
hj : j ∈ is
snd : v.elim (α := α) ⋯ = TProd.elim (α := α) w.2 hj
snd₁ : w.elim (α := α) ⋯ = TProd.elim (α := α) w.2 hj
⊢ TProd.elim (α := α) v.2 hj = TProd.elim (α := α) w.2 hj
have snd₂ : TProd.elim (α := α) w.2 hj = TProd.elim (α := α) w.2 hj
Tactic: rw [← elim_of_mem hl, hvw, elim_of_mem hl]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
⊢ TProd.mk (α := α) (i :: l) ⁻¹' Set.tprod (α := α) (i :: l) t = pi (α := α) {i_1 : ι | i_1 ∈ i :: l} t
have h : ∀ (f : (i : ι) → α i),
  f ∈ TProd.mk (α := α) (i :: l) ⁻¹' Set.tprod (α := α) (i :: l) t ↔ f ∈ pi (α := α) {i_1 : ι | i_1 ∈ i :: l} t
Tactic: ext f
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
have change : f ∈ TProd.mk (α := α) l ⁻¹' Set.tprod (α := α) l t ↔ f ∈ pi (α := α) {x : ι | x ∈ l} t
Tactic: change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ { x | x ∈ l }.pi t
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk (α := α) l ⁻¹' Set.tprod (α := α) l t ↔ f ∈ pi (α := α) {x : ι | x ∈ l} t
have rw : f ∈ pi (α := α) {i : ι | i ∈ l} t ↔ f ∈ pi (α := α) {x : ι | x ∈ l} t
Tactic: rw [mk_preimage_tprod l t]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (hypothesis)
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk (α := α) (i :: l) ⁻¹' Set.tprod (α := α) (i :: l) t ↔ f ∈ pi (α := α) {i_1 : ι | i_1 ∈ i :: l} t
have h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
Tactic: have h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i := by
      change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ { x | x ∈ l }.pi t
      rw [mk_preimage_tprod l t]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f ∈ TProd.mk (α := α) (i :: l) ⁻¹' Set.tprod (α := α) (i :: l) t ↔ f ∈ pi (α := α) {i_1 : ι | i_1 ∈ i :: l} t
have h₁ : f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔
  ∀ (i_1 : ι), Membership.mem (γ := Set ι) {i_2 : ι | i_2 ∈ i :: l} i_1 → f i_1 ∈ t i_1
Tactic: rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prodMk_mem_set_prod_eq]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔
    ∀ (i_1 : ι), Membership.mem (γ := Set ι) {i_2 : ι | i_2 ∈ i :: l} i_1 → f i_1 ∈ t i_1
have h₁ : f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1
Tactic: simp_rw [mem_setOf_eq, mem_cons]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1
have h₁ : f i ∈ t i → (TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (a : ι), a ∈ l → f a ∈ t a)
Tactic: rw [forall_eq_or_imp, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ
have h₁ : ∀ (i : ι), Membership.mem (γ := Set ι) {i : ι | i ∈ l} i ↔ Membership.mem (γ := Set ι) univ i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (hypothesis)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ TProd.elim' (α := α) h ⁻¹' pi (α := α) univ t = Set.tprod (α := α) l t
have h2 : Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ
Tactic: have h2 : { i | i ∈ l } = univ := by
    ext i
    simp [h]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ
⊢ TProd.elim' (α := α) h ⁻¹' pi (α := α) univ t = Set.tprod (α := α) l t
have rw : (fun (x : TProd α l) ↦ TProd.mk (α := α) l (TProd.elim' (α := α) h x)) ⁻¹' Set.tprod (α := α) l t =
  Set.tprod (α := α) l t
Tactic: rw [← h2, ← mk_preimage_tprod, preimage_preimage]
-- Lean 4 proof step from Mathlib.Data.Prod.TProd (goal)
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ
⊢ (fun (x : TProd α l) ↦ TProd.mk (α := α) l (TProd.elim' (α := α) h x)) ⁻¹' Set.tprod (α := α) l t =
    Set.tprod (α := α) l t
have simp : (fun (x : TProd α l) ↦ x) ⁻¹' Set.tprod (α := α) l t = Set.tprod (α := α) l t
Tactic: simp only [TProd.mk_elim hnd h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ map (F := F) (α := α) (β := α) (TypeVec.id (α := α)) x = x
have rw : abs (F := F) (α := α)
    (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := α) (TypeVec.id (α := α))
      (repr (F := F) (α := α) x)) =
  abs (F := F) (α := α) (repr (F := F) (α := α) x)
Tactic: rw [← abs_repr x, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ map (F := F) (α := α) (β := γ) (TypeVec.comp (α := α) (β := β) (γ := γ) g f) x =
    map (F := F) (α := β) (β := γ) g (map (F := F) (α := α) (β := β) f x)
have rw : abs (F := F) (α := γ)
    (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := γ) (TypeVec.comp (α := α) (β := β) (γ := γ) g f)
      (repr (F := F) (α := α) x)) =
  abs (F := F) (α := γ)
    (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := β) (β := γ) g
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f (repr (F := F) (α := α) x)))
Tactic: rw [← abs_repr x, ← abs_map, ← abs_map, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP (F := F) (α := α) p x ↔
    ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
have mp : LiftP (F := F) (α := α) p x →
  ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
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
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
mp :
  LiftP (F := F) (α := α) p x →
    ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ LiftP (F := F) (α := α) p x ↔
    ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
have mpr : (∃ (a : (P F).A) (f : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)) →
  LiftP (F := F) (α := α) p x
Tactic: constructor