case inl
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded (Pi.Lex r fun {i} => s i)

case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
⊢ WellFounded (Pi.Lex r fun {i} => s i)
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
⊢ WellFounded (Pi.Lex r fun {i} => s i)
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
⊢ WellFounded (Pi.Lex r fun {i} => s i)
letI : ∀ i, Zero (α i) := fun i => ⟨(hs i).min ⊤ ⟨x i, trivial⟩⟩
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this : IsTrans ι (Function.swap r)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
⊢ WellFounded (Pi.Lex r fun {i} => s i)
haveI := IsTrans.swap r
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝¹ : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝ : IsTrans ι (Function.swap r)
this : IsIrrefl ι (Function.swap r)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this : IsTrans ι (Function.swap r)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
haveI := IsIrrefl.swap r
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
⊢ WellFounded (Pi.Lex r fun {i} => s i)
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝¹ : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝ : IsTrans ι (Function.swap r)
this : IsIrrefl ι (Function.swap r)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
haveI := Fintype.ofFinite ι
case inr.intro.refine'_1
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
i : ι
a : α i
⊢ ¬s i a 0

case inr.intro.refine'_2
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
⊢ WellFounded (Function.swap fun j i => r j i)
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
⊢ WellFounded (Pi.Lex r fun {i} => s i)
refine' InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => _) hs _)
no goals
case inr.intro.refine'_1
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
i : ι
a : α i
⊢ ¬s i a 0

case inr.intro.refine'_2
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
⊢ WellFounded (Function.swap fun j i => r j i)
exacts [(hs i).not_lt_min ⊤ _ trivial, Finite.wellFounded_of_trans_of_irrefl (Function.swap r)]
no goals
case inl
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
convert emptyWf.wf