awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ((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
simp_rw₂ : a < x i ∨ update (β := β) x i a = x ↔ 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

Tactic:
simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]

Premises used: toLex_inj, Pi.toLex_update_lt_self_iff, le_iff_lt_or_eq, Function.update_eq_self_iff
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedGT ι
⊢ Monotone (α := (i : ι) → β i) (β := Colex ((i : ι) → β i)) (⇑toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i))

Tactic:
toLex_monotone (ι := ιᵒᵈ)

Premises used: Colex, OrderDual, Pi.toLex_monotone
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → PartialOrder (β i)
inst_2 : WellFoundedGT ι
⊢ StrictMono (α := (i : ι) → β i) (β := Colex ((i : ι) → β i)) (⇑toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i))

Tactic:
toLex_strictMono (ι := ιᵒᵈ)

Premises used: Colex, OrderDual, 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 : WellFoundedGT ι
⊢ LT.lt (α := Colex ((i : ι) → β i)) ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i))
      ((toColex : (a : (a : ι) → β a) → Colex ((a : ι) → β a)) (update (β := β) x i a) : Colex ((a : ι) → β a)) ↔
    x i < a

Tactic:
lt_toLex_update_self_iff (ι := ιᵒᵈ)

Premises used: Pi.lt_toLex_update_self_iff, OrderDual
-- 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 : WellFoundedGT ι
⊢ LT.lt (α := Colex ((a : ι) → β a))
      ((toColex : (a : (a : ι) → β a) → Colex ((a : ι) → β a)) (update (β := β) x i a) : Colex ((a : ι) → β a))
      ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i)) ↔
    a < x i

Tactic:
toLex_update_lt_self_iff (ι := ιᵒᵈ)

Premises used: Pi.toLex_update_lt_self_iff, OrderDual
-- 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 : WellFoundedGT ι
⊢ LE.le (α := Colex ((i : ι) → β i)) ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i))
      ((toColex : (a : (a : ι) → β a) → Colex ((a : ι) → β a)) (update (β := β) x i a) : Colex ((a : ι) → β a)) ↔
    x i ≤ a

Tactic:
le_toLex_update_self_iff (ι := ιᵒᵈ)

Premises used: Colex, Pi.le_toLex_update_self_iff, OrderDual
-- 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 : WellFoundedGT ι
⊢ LE.le (α := Colex ((a : ι) → β a))
      ((toColex : (a : (a : ι) → β a) → Colex ((a : ι) → β a)) (update (β := β) x i a) : Colex ((a : ι) → β a))
      ((toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x : Colex ((i : ι) → β i)) ↔
    a ≤ x i

Tactic:
toLex_update_le_self_iff (ι := ιᵒᵈ)

Premises used: Colex, Pi.toLex_update_le_self_iff, OrderDual
-- Module: Mathlib.Order.PiLex
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
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))
⊢ x i ≤ y i

Tactic:
contrapose! hxy
-- Module: Mathlib.Order.PiLex
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
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))
⊢ ¬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:
apply not_le_of_gt

Premises used: not_le_of_gt
-- Module: Mathlib.Order.PiLex
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
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)
⊢ 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:
use i
-- Module: Mathlib.Order.PiLex
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
⊢ (∀ (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:
aesop
-- Module: Mathlib.Order.PiLex
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
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))
⊢ x i ≤ y i

Tactic:
contrapose! hxy
-- Module: Mathlib.Order.PiLex
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
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))
⊢ ¬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:
apply not_le_of_gt

Premises used: not_le_of_gt
-- Module: Mathlib.Order.PiLex
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
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)
⊢ 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:
use i
-- Module: Mathlib.Order.PiLex
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
⊢ (∀ (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:
aesop
-- Module: Mathlib.Order.PiLex
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
obtain : ∀ (a : β i) (ha₁ : a₁ i < a) (ha₂ : a < a₂ i), ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := exists_between hi

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

Tactic:
⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩

Premises used: Function.update, And.intro, Exists.intro
-- Module: Mathlib.Order.PiLex
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
refine_4 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (Function.update (β := β) a₂ i a i) (a₂ i)
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂

Tactic:
refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
-- Module: Mathlib.Order.PiLex
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
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
refine_1 : a₂ j = Function.update (β := β) a₂ i a j
⊢ a₁ j = Function.update (β := β) a₂ i a j

Tactic:
rw [h j hj]
-- Module: Mathlib.Order.PiLex
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
j : ι
hj : j < i
refine_1 refine_1₁ : a₂ j = a₂ j
⊢ a₂ j = Function.update (β := β) a₂ i a j

Tactic:
rw [Function.update_of_ne hj.ne a]

Premises used: LT.lt.ne, Function.update_of_ne
-- Module: Mathlib.Order.PiLex
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_2 refine_2₁ refine_2₂ refine_2₃ : a₁ i < a
⊢ (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (a₁ i) (Function.update (β := β) a₂ i a i)

Tactic:
rwa [Function.update_self i a]

Premises used: Function.update_self
-- Module: Mathlib.Order.PiLex
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
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
refine_3 refine_3₁ : a₂ j = a₂ j
⊢ Function.update (β := β) a₂ i a j = a₂ j

Tactic:
rw [Function.update_of_ne hj.ne a]

Premises used: LT.lt.ne, Function.update_of_ne
-- Module: Mathlib.Order.PiLex
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₂ refine_4 refine_4₁ refine_4₂ refine_4₃ : a < a₂ i
⊢ (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (Function.update (β := β) a₂ i a i) (a₂ i)

Tactic:
rwa [Function.update_self i a]

Premises used: Function.update_self
-- Module: Mathlib.Order.PiLex
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
refine_4 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (Function.update (β := β) a₂ i a i) (a₂ i)
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
refine_4₁ : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (Function.update (β := β) a₂ i a i) (a₂ i)
refine_3₂ : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), Function.update (β := β) a₂ i a j = a₂ j
refine_4₂ refine_4₃ : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (Function.update (β := β) a₂ i a i) (a₂ i)
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂

Tactic:
classical
      refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
      · rw [h j hj]
        dsimp only at hj
        rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
      · rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
-- Module: Mathlib.Order.PiLex
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)
⊢ DenselyOrdered (Colex ((i : ι) → β i))

Tactic:
inferInstanceAs (DenselyOrdered (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))

Premises used: _private.0.Pi.instDenselyOrderedColexForall._proof_1
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
i : ι
inst_2 : NoMaxOrder.{u_2} (β i)
a : Lex ((i : ι) → β i)
let : ∀ (b : β i) (hb : a i < b), ∃ (b : Lex ((i : ι) → β i)), a < b
⊢ ∃ (b : Lex ((i : ι) → β i)), a < b

Tactic:
let ⟨b, hb⟩ := exists_gt (a i)
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
i : ι
inst_2 : NoMaxOrder.{u_2} (β i)
a : Lex ((i : ι) → β i)
b : β i
hb rwa rwa₁ rwa₂ rwa₃ : a i < b
⊢ a i < Function.update (β := β) a i b i

Tactic:
rwa [Function.update_self i b]

Premises used: Function.update_self
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
i : ι
inst_2 : NoMaxOrder.{u_2} (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ (b : Lex ((i : ι) → β i)), a < b

Tactic:
exact ⟨Function.update a i b, i, fun j hj =>
      (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
i : ι
inst_2 : NoMaxOrder.{u_2} (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ (b : Lex ((i : ι) → β i)), a < b

Tactic:
classical
    exact ⟨Function.update a i b, i, fun j hj =>
      (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
i : ι
inst_2 : NoMaxOrder.{u_2} (β i)
⊢ NoMaxOrder (Colex ((i : ι) → β i))

Tactic:
Lex.noMaxOrder' (ι := ιᵒᵈ) i

Premises used: Colex, OrderDual, Pi.Lex.noMaxOrder'
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Nonempty ι
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : ∀ (i : ι), NoMaxOrder.{u_2} (β i)
⊢ NoMaxOrder (Lex ((i : ι) → β i))

Tactic:
⟨fun a =>
    let ⟨_, hb⟩ := exists_gt (ofLex a)
    ⟨_, toLex_strictMono hb⟩⟩

Premises used: Exists, NoMaxOrder.mk, NoMaxOrder.exists_gt, LT.lt, _private.0.Pi.instNoMaxOrderLexForallOfWellFoundedLTOfNonempty.match_1, Exists.intro, ofLex, DFunLike.coe, Pi.toLex_strictMono, toLex
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : WellFoundedGT ι
inst_2 : Nonempty ι
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : ∀ (i : ι), NoMaxOrder.{u_2} (β i)
⊢ NoMaxOrder (Colex ((i : ι) → β i))

Tactic:
inferInstanceAs (NoMaxOrder (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))

Premises used: _private.0.Pi.instNoMaxOrderColexForallOfWellFoundedGTOfNonempty._proof_1
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Nonempty ι
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : ∀ (i : ι), NoMinOrder.{u_2} (β i)
⊢ NoMinOrder (Lex ((i : ι) → β i))

Tactic:
⟨fun a =>
    let ⟨_, hb⟩ := exists_lt (ofLex a)
    ⟨_, toLex_strictMono hb⟩⟩

Premises used: Exists, NoMinOrder.mk, LT.lt, Exists.intro, NoMinOrder.exists_lt, ofLex, DFunLike.coe, _private.0.Pi.instNoMinOrderLexForallOfWellFoundedLTOfNonempty.match_1, Pi.toLex_strictMono, toLex
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : WellFoundedGT ι
inst_2 : Nonempty ι
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : ∀ (i : ι), NoMinOrder.{u_2} (β i)
⊢ NoMinOrder (Colex ((i : ι) → β i))

Tactic:
inferInstanceAs (NoMinOrder (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))

Premises used: _private.0.Pi.instNoMinOrderColexForallOfWellFoundedGTOfNonempty._proof_1
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : DecidableEq ι
inst_2 : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f j < f i
⊢ (@fun {i : ι} (x1 x2 : (fun (a : ι) ↦ α) i) ↦ x1 < x2) i
    ((toLex : (a : ι → α) → Lex (ι → α)) (f ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) i)
    ((toLex : (a : ι → α) → Lex (ι → α)) f i)

Tactic:
simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂

Premises used: Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : DecidableEq ι
inst_2 : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
rw :
  LT.lt (α := Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) (f ∘ (⇑(Equiv.swap j i) : (a : ι) → ι)) : Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) f : Colex (ι → α))
⊢ LT.lt (α := Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) (f ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) f : Colex (ι → α))

Tactic:
rw [Equiv.swap_comm]

Premises used: Equiv.swap_comm
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : DecidableEq ι
inst_2 : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
⊢ LT.lt (α := Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) (f ∘ (⇑(Equiv.swap j i) : (a : ι) → ι)) : Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) f : Colex (ι → α))

Tactic:
lex_desc (ι := ιᵒᵈ) h₁ h₂

Premises used: Pi.lex_desc, OrderDual
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : DecidableEq ι
inst_2 : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
⊢ LT.lt (α := Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) (f ∘ (⇑(Equiv.swap j i) : (a : ι) → ι)) : Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) f : Colex (ι → α))

Tactic:
exact lex_desc (ι := ιᵒᵈ) h₁ h₂
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsChain r ∅

Tactic:
pairwise_empty _

Premises used: Set.pairwise_empty, IsChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
a : α
⊢ IsChain r {a}

Tactic:
pairwise_singleton ..

Premises used: Set.pairwise_singleton, IsChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : s.Subsingleton
⊢ IsChain r s

Tactic:
hs.pairwise _

Premises used: Set.Subsingleton.pairwise, IsChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ s ⊆ t → IsChain r t → IsChain r s

Tactic:
Set.Pairwise.mono

Premises used: Set.Pairwise.mono, IsChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
r' : α → α → Prop
h : IsChain r s
h_imp : ∀ (x y : α), r x y → r' x y
⊢ IsChain r' s

Tactic:
h.mono' fun x y => Or.imp (h_imp x y) (h_imp y x)

Premises used: IsChain, Set.Pairwise.mono', Or.imp
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsChain r s
⊢ IsChain (flip r) s

Tactic:
h.mono' fun _ _ => Or.symm

Premises used: Or.symm, IsChain, Set.Pairwise.mono'
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
s : Set α
⊢ IsChain r s

Tactic:
fun a _ b _ hab => (trichotomous_of r a b).imp_right fun h => h.resolve_left hab

Premises used: Set.Pairwise, IsChain, trichotomous_of, Or.imp_right
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hs : IsChain r s
ha : ∀ b ∈ s, a ≠ b → r a b ∨ r b a
⊢ IsChain r (insert a s)

Tactic:
hs.insert_of_symmetric (fun _ _ => Or.symm) ha

Premises used: Or.symm, IsChain, Set.Pairwise.insert_of_symmetric