-- Mathlib/Order/PiLex.lean
theorem toLex_update_lt_self_iff : toLex (update x i a) < toLex x ↔ a < x i

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : update x i a j < x j
H : ¬j = i
⊢ False

Tactic:
rw [update_of_ne H] at h

Result:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : x j < x j
H : ¬j = i
⊢ False

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : x j < x j
H : ¬j = i
⊢ False

Tactic:
exact h.false

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : toLex (update x i a) j < toLex x j
⊢ a < x i

Tactic:
dsimp at h

Result:
case intro.intro
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : update x i a j < x j
⊢ a < x i

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
⊢ toLex (update x i a) < toLex x ↔ a < x i

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

Result:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
⊢ toLex (update x i a) < toLex x → a < x i

Proof state:
case intro.intro
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x j a) j_1 = toLex x j_1
h : update x j a j < x j
⊢ a < x j

Tactic:
rwa [update_self] at h

Result:
no goals

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
⊢ toLex (update x i a) < toLex x → a < x i

Tactic:
rintro ⟨j, hj, h⟩

Result:
case intro.intro
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : toLex (update x i a) j < toLex x j
⊢ a < x i

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : update x i a j < x j
⊢ j = i

Tactic:
by_contra H

Result:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : update x i a j < x j
H : ¬j = i
⊢ False

Proof state:
case intro.intro
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : update x i a j < x j
⊢ a < x i

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

Result:
case intro.intro
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x1 x2 => x1 < x2) j_1 j → toLex (update x j a) j_1 = toLex x j_1
h : update x j a j < x j
⊢ a < x j