awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
a b : (i : ι) → β i
h : a ≤ b
hne :
  ¬Eq (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) a : Lex ((i : ι) → β i))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) b : Lex ((i : ι) → β i))
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | a i ≠ b i} i
hl : ∀ (x : ι), Membership.mem (γ := Set ι) {i : ι | a i ≠ b i} x → ¬x < i
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
⊢ Eq.{u_2 + 1} (α := β j) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) a j : β j)
    ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) b j : β j)
have contrapose! : ∀
  (hl :
    Ne.{u_2 + 1} (α := β j) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) a j : β j)
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) b j : β j)),
  ∃ (x : ι), Membership.mem (γ := Set ι) {i : ι | a i ≠ b i} x ∧ x < i
Tactic: contrapose! hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
a b : (i : ι) → β i
h : a < b
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | a i ≠ b i} i
hl : ∀ (x : ι), Membership.mem (γ := Set ι) {i : ι | a i ≠ b i} x → ¬x < i
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
⊢ Eq.{u_2 + 1} (α := β j) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) a j : β j)
    ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) b j : β j)
have contrapose! : ∀
  (hl :
    Ne.{u_2 + 1} (α := β j) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) a j : β j)
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) b j : β j)),
  ∃ (x : ι), Membership.mem (γ := Set ι) {i : ι | a i ≠ b i} x ∧ x < i
Tactic: contrapose! hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
⊢ LT.lt (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
    x i < a
have refine : LT.lt (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
    ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) →
  x i < a
Tactic: refine ⟨?_, fun h => toLex_strictMono <| lt_update_self_iff.2 h⟩
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) j_1 : β j_1)
h : x j < update (β := β) x i a j
⊢ j = i
have by_contra : ∀ (H : ¬j = i), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Order.PiLex (hypothesis)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) j_1 : β j_1)
h : x j < update (β := β) x i a j
H : ¬j = i
⊢ False
have h₁ : x j < x j
Tactic: rw [update_of_ne H] at h
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) j_1 : β j_1)
h : x j < update (β := β) x i a j
⊢ x i < a
have obtain : ∀ {a : β j}
  (hj :
    ∀ (j_1 : ι),
      (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
        Eq.{u_2 + 1} (α := β j_1) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
          ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x j a) j_1 : β j_1))
  (h : x j < update (β := β) x j a j), x j < a
Tactic: obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false
Cleared hypotheses: i, a, hj, h
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
a : β j
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x j a) j_1 : β j_1)
h : x j < update (β := β) x j a j
⊢ x j < a
have rwa : ∀ (h : x j < a), x j < a
Tactic: rwa [update_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
⊢ LT.lt (α := Lex ((a : ι) → β a))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
    a < x i
have refine : LT.lt (α := Lex ((a : ι) → β a))
    ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
    ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) →
  a < x i
Tactic: refine ⟨?_, fun h => toLex_strictMono <| update_lt_self_iff.2 h⟩
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) j_1 : β j_1)
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
h : update (β := β) x i a j < x j
⊢ j = i
have by_contra : ∀ (H : ¬j = i), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Order.PiLex (hypothesis)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) j_1 : β j_1)
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
h : update (β := β) x i a j < x j
H : ¬j = i
⊢ False
have h₁ : x j < x j
Tactic: rw [update_of_ne H] at h
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) j_1 : β j_1)
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
h : update (β := β) x i a j < x j
⊢ a < x i
have obtain : ∀ {a : β j}
  (hj :
    ∀ (j_1 : ι),
      (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
        Eq.{u_2 + 1} (α := β j_1)
          ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x j a) j_1 : β j_1)
          ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1))
  (h : update (β := β) x j a j < x j), a < x j
Tactic: obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false
Cleared hypotheses: i, a, hj, h
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
j : ι
a : β j
hj :
  ∀ (j_1 : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j_1 j →
      Eq.{u_2 + 1} (α := β j_1)
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x j a) j_1 : β j_1)
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j_1 : β j_1)
h : update (β := β) x j a j < x j
⊢ a < x j
have rwa : ∀ (h : a < x j), a < x j
Tactic: rwa [update_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
⊢ LE.le (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
    x i ≤ a
have simp_rw : LT.lt (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ∨
    Eq (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
  x i < a ∨ x i = a
Tactic: simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
simp_rw :
  LT.lt (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ∨
      Eq (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
    x i < a ∨ x i = a
⊢ LE.le (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
    x i ≤ a
have simp_rw₁ : x i < a ∨
    Eq (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
  x i < a ∨ x i = a
Tactic: simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
simp_rw :
  LT.lt (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ∨
      Eq (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
    x i < a ∨ x i = a
simp_rw₁ :
  x i < a ∨
      Eq (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
    x i < a ∨ x i = a
⊢ LE.le (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a)) ↔
    x i ≤ a
have simp_rw₂ : x i < a ∨ x = update (β := β) x i a ↔ x i < a ∨ x i = a
Tactic: simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
⊢ LE.le (α := Lex ((a : ι) → β a))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
    a ≤ x i
have simp_rw : LT.lt (α := Lex ((a : ι) → β a))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ∨
    Eq (α := Lex ((a : ι) → β a))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
  a < x i ∨ a = x i
Tactic: simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
simp_rw :
  LT.lt (α := Lex ((a : ι) → β a))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ∨
      Eq (α := Lex ((a : ι) → β a))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
    a < x i ∨ a = x i
⊢ LE.le (α := Lex ((a : ι) → β a))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
    a ≤ x i
have simp_rw₁ : a < x i ∨
    Eq (α := Lex ((a : ι) → β a))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
  a < x i ∨ a = x i
Tactic: simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
simp_rw :
  LT.lt (α := Lex ((a : ι) → β a))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ∨
      Eq (α := Lex ((a : ι) → β a))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
    a < x i ∨ a = x i
simp_rw₁ :
  a < x i ∨
      Eq (α := Lex ((a : ι) → β a))
        ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
    a < x i ∨ a = x i
⊢ LE.le (α := Lex ((a : ι) → β a))
      ((toLex : (a : (a : ι) → β a) → Lex ((a : ι) → β a)) (update (β := β) x i a) : Lex ((a : ι) → β a))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i)) ↔
    a ≤ x i
have simp_rw₂ : a < x i ∨ update (β := β) x i a = x ↔ a < x i ∨ a = x i
Tactic: simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst_1 : (i : ι) → LinearOrder (β i)
hxy :
  LE.le (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
    ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) y : Lex ((i : ι) → β i))
h : ∀ (j : ι), j < i → x j = y j
⊢ x i ≤ y i
have contrapose! : ∀ (hxy : y i < x i),
  ¬LE.le (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) y : Lex ((i : ι) → β i))
Tactic: contrapose! hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst_1 : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j < i → x j = y j
hxy : y i < x i
⊢ ¬LE.le (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
      ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) y : Lex ((i : ι) → β i))
have hab : LT.lt (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) y : Lex ((i : ι) → β i))
  ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
Tactic: apply not_le_of_gt
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst_1 : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j < i → x j = y j
hxy : y i < x i
⊢ LT.lt (α := Lex ((i : ι) → β i)) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) y : Lex ((i : ι) → β i))
    ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x : Lex ((i : ι) → β i))
have h₁ : (∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j i →
      Eq.{u_2 + 1} (α := β j) ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) y j : β j)
        ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x j : β j)) ∧
  (@fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) i ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) y i)
    ((toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x i)
Tactic: use i
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst_1 : (i : ι) → LinearOrder (β i)
hxy :
  LE.le (α := Colex ((i : ι) → β i)) ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i))
    ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) y : Colex ((i : ι) → β i))
h : ∀ (j : ι), j > i → x j = y j
⊢ x i ≤ y i
have contrapose! : ∀ (hxy : y i < x i),
  ¬LE.le (α := Colex ((i : ι) → β i))
      ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i))
      ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) y : Colex ((i : ι) → β i))
Tactic: contrapose! hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst_1 : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j > i → x j = y j
hxy : y i < x i
⊢ ¬LE.le (α := Colex ((i : ι) → β i))
      ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i))
      ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) y : Colex ((i : ι) → β i))
have hab : LT.lt (α := Colex ((i : ι) → β i)) ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) y : Colex ((i : ι) → β i))
  ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i))
Tactic: apply not_le_of_gt
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst_1 : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j > i → x j = y j
hxy : y i < x i
⊢ LT.lt (α := Colex ((i : ι) → β i)) ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) y : Colex ((i : ι) → β i))
    ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i))
have h₁ : (∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 > x2) j i →
      Eq.{u_2 + 1} (α := β j) ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) y j : β j)
        ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x j : β j)) ∧
  (@fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) i ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) y i)
    ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x i)
Tactic: use i
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have obtain : ∀ (a : β i) (ha₁ : a₁ i < a) (ha₂ : a < a₂ i), ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
Tactic: obtain ⟨a, ha₁, ha₂⟩ := exists_between hi
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
Tactic: refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_2 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (a₁ i) (Function.update (β := β) a₂ i a i)
Tactic: refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
refine_2 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (a₁ i) (Function.update (β := β) a₂ i a i)
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_3 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), Function.update (β := β) a₂ i a j = a₂ j
Tactic: refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
refine_2 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (a₁ i) (Function.update (β := β) a₂ i a i)
refine_3 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), Function.update (β := β) a₂ i a j = a₂ j
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_4 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (Function.update (β := β) a₂ i a i) (a₂ i)
Tactic: refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩