case mp
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd

case mpr
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b ↔ ∃ h, h ▸ a.snd ≤ b.snd
constructor
case mp.fiber
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ h, h ▸ { fst := i, snd := a }.snd ≤ { fst := i, snd := b }.snd
case mp
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd
rintro ⟨i, a, b, h⟩
no goals
case mp.fiber
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ h, h ▸ { fst := i, snd := a }.snd ≤ { fst := i, snd := b }.snd
exact ⟨rfl, h⟩
case mpr.mk
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ { fst := i, snd := a }.snd ≤ b.snd) → { fst := i, snd := a } ≤ b
case mpr
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b
obtain ⟨i, a⟩ := a
case mpr.mk.mk
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ { fst := i, snd := a }.snd ≤ { fst := j, snd := b }.snd) → { fst := i, snd := a } ≤ { fst := j, snd := b }
case mpr.mk
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ { fst := i, snd := a }.snd ≤ b.snd) → { fst := i, snd := a } ≤ b
obtain ⟨j, b⟩ := b
case mpr.mk.mk.intro
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : (_ : i = i) ▸ { fst := i, snd := a }.snd ≤ { fst := i, snd := b }.snd
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b }
case mpr.mk.mk
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ { fst := i, snd := a }.snd ≤ { fst := j, snd := b }.snd) → { fst := i, snd := a } ≤ { fst := j, snd := b }
rintro ⟨rfl : i = j, h⟩
no goals
case mpr.mk.mk.intro
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : (_ : i = i) ▸ { fst := i, snd := a }.snd ≤ { fst := i, snd := b }.snd
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b }
exact le.fiber _ _ _ h