ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ ↑toLex a ≤ ↑toLex b
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ Monotone ↑toLex
intro a b h
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
⊢ ↑toLex a < ↑toLex b
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ ↑toLex a ≤ ↑toLex b
refine' le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ _)
no goals
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
⊢ ↑toLex a < ↑toLex b
classical
exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
  fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
  (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩
no goals
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
⊢ ↑toLex a < ↑toLex b
exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
  fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
  (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩