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

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 x j_1 = toLex (update x i a) 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 x j_1 = toLex (update x i a) j_1
h : x j < update x i a j
⊢ x i < a

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 x j_1 = toLex (update x j a) j_1
h : x j < update x j a j
⊢ x j < a

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 x j_1 = toLex (update x i a) j_1
h : toLex x j < toLex (update x i a) j
⊢ x i < a

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 x j_1 = toLex (update x i a) j_1
h : x j < update x i a j
⊢ x i < a

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 x j_1 = toLex (update x i a) j_1
h : x j < update x i a 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 x j_1 = toLex (update x i a) 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 x j_1 = toLex (update x i a) j_1
h : x j < update x i a 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 x j_1 = toLex (update x i a) j_1
h : x j < update x i a 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
⊢ toLex x < toLex (update x i a) → x i < a

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 x j_1 = toLex (update x i a) j_1
h : toLex x j < toLex (update x i a) j
⊢ x i < a

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 x j_1 = toLex (update x j a) j_1
h : x j < update x j a j
⊢ x j < a

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 x < toLex (update x i a) ↔ x i < a

Tactic:
refine ⟨?_, fun h => toLex_strictMono <| lt_update_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 x < toLex (update x i a) → x i < a