awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → b j = c j
b_lt_c : b N₁ < c N₁
⊢ a < c

Tactic:
⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ hj), a_lt_b.trans b_lt_c⟩

Premises used: Pi.Lex, And.intro, Exists.intro, LT.lt.trans, Eq.trans
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₂ < N₁
⊢ a < c

Tactic:
⟨N₂, fun j hj => (lt_N₁ _ (hj.trans H)).trans (lt_N₂ _ hj), (lt_N₁ _ H).symm ▸ b_lt_c⟩

Premises used: Eq.rec, Pi.Lex, And.intro, Exists.intro, LT.lt.trans, Eq.symm, Eq.trans
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₁ < N₂
⊢ a < c

Tactic:
exacts [⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ <| hj.trans H), lt_N₂ _ H ▸ a_lt_b⟩,
      ⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ hj), a_lt_b.trans b_lt_c⟩,
      ⟨N₂, fun j hj => (lt_N₁ _ (hj.trans H)).trans (lt_N₂ _ hj), (lt_N₁ _ H).symm ▸ b_lt_c⟩]
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
⊢ IsStrictOrder (Colex ((i : ι) → β i)) fun (x1 x2 : Colex ((i : ι) → β i)) ↦ x1 < x2

Tactic:
Lex.isStrictOrder (ι := ιᵒᵈ)

Premises used: Colex, OrderDual, Pi.Lex.isStrictOrder
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₂ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq (α := (i : ι) → β i) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
        ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₃ :
  (LT.lt (α := β default) (x default) (y default) ∨
      ∀ (x_1 : ι),
        Eq.{u_2 + 1} (α := β x_1) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x x_1 : β x_1)
          ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y x_1 : β x_1)) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₄ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq.{u_2 + 1} (α := β default) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x default : β default)
        ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y default : β default) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)

Tactic:
simp_rw [le_iff_lt_or_eq, Pi.Lex.lt_iff_of_unique, ← ofLex_inj, funext_iff, Unique.forall_iff,
    ofLex_apply]

Premises used: Pi.ofLex_apply, funext_iff, Unique.forall_iff, le_iff_lt_or_eq, ofLex_inj, Pi.Lex.lt_iff_of_unique
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₂ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq (α := (i : ι) → β i) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
        ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₃ :
  (LT.lt (α := β default) (x default) (y default) ∨
      ∀ (x_1 : ι),
        Eq.{u_2 + 1} (α := β x_1) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x x_1 : β x_1)
          ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y x_1 : β x_1)) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₄ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq.{u_2 + 1} (α := β default) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x default : β default)
        ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y default : β default) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)

Tactic:
simp_rw [le_iff_lt_or_eq, Pi.Colex.lt_iff_of_unique, ← ofColex_inj, funext_iff, Unique.forall_iff,
    ofColex_apply]

Premises used: Pi.Colex.lt_iff_of_unique, funext_iff, Pi.ofColex_apply, Unique.forall_iff, ofColex_inj, le_iff_lt_or_eq
-- Module: Mathlib.Order.PiLex
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
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
⊢ 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)

Tactic:
contrapose! hl
-- Module: Mathlib.Order.PiLex
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
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
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:
⟨j, hl, hj⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.PiLex
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
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
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:
exact ⟨j, hl, hj⟩
-- Module: Mathlib.Order.PiLex
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
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
⊢ 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)

Tactic:
contrapose! hl
-- Module: Mathlib.Order.PiLex
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
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
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:
⟨j, hl, hj⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.PiLex
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
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
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:
exact ⟨j, hl, hj⟩
-- Module: Mathlib.Order.PiLex
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

Tactic:
⟨?_, fun h => toLex_strictMono <| lt_update_self_iff.2 h⟩

Premises used: Iff.mpr, lt_update_self_iff, Iff.intro, Pi.toLex_strictMono
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
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
⊢ 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⟩
-- Module: Mathlib.Order.PiLex
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
by_contra : ∀ (H : ¬j = i), False
⊢ j = i

Tactic:
by_contra H
-- Module: Mathlib.Order.PiLex
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
⊢ x j < x j

Tactic:
rw [update_of_ne H] at h

Premises used: Function.update_of_ne
-- Module: Mathlib.Order.PiLex
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
h₁ : x j < x j
⊢ ¬j = i

Tactic:
rw [update_of_ne H] at h

Premises used: Function.update_of_ne
-- Module: Mathlib.Order.PiLex
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 < x j
H : ¬j = i
⊢ False

Tactic:
h.false

Premises used: LT.lt.false
-- Module: Mathlib.Order.PiLex
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 < x j
H : ¬j = i
⊢ False

Tactic:
exact h.false

Premises used: LT.lt.false
-- Module: Mathlib.Order.PiLex
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
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
⊢ x i < a

Tactic:
obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false

Premises used: rfl
-- Module: Mathlib.Order.PiLex
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : x j < a), x j < a
⊢ x j < a

Tactic:
rwa [update_self] at h

Premises used: Function.update_self
-- Module: Mathlib.Order.PiLex
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

Tactic:
⟨?_, fun h => toLex_strictMono <| update_lt_self_iff.2 h⟩

Premises used: Iff.mpr, Iff.intro, update_lt_self_iff, Pi.toLex_strictMono
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedLT ι
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
⊢ 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⟩
-- Module: Mathlib.Order.PiLex
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
by_contra : ∀ (H : ¬j = i), False
⊢ j = i

Tactic:
by_contra H
-- Module: Mathlib.Order.PiLex
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
⊢ x j < x j

Tactic:
rw [update_of_ne H] at h

Premises used: Function.update_of_ne
-- Module: Mathlib.Order.PiLex
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
h₁ : x j < x j
⊢ ¬j = i

Tactic:
rw [update_of_ne H] at h

Premises used: Function.update_of_ne
-- Module: Mathlib.Order.PiLex
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 : x j < x j
H : ¬j = i
⊢ False

Tactic:
h.false

Premises used: LT.lt.false
-- Module: Mathlib.Order.PiLex
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 : x j < x j
H : ¬j = i
⊢ False

Tactic:
exact h.false

Premises used: LT.lt.false
-- Module: Mathlib.Order.PiLex
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
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
⊢ a < x i

Tactic:
obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false

Premises used: rfl
-- Module: Mathlib.Order.PiLex
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : a < x j), a < x j
⊢ a < x j

Tactic:
rwa [update_self] at h

Premises used: Function.update_self
-- Module: Mathlib.Order.PiLex
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
simp_rw₂ : x i < a ∨ x = update (β := β) x i 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

Tactic:
simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]

Premises used: toLex_inj, Function.eq_update_self_iff, le_iff_lt_or_eq, Pi.lt_toLex_update_self_iff