[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
h : { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
⊢ a₁ = a₂ ∧ HEq b₁ b₂
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ : α
b₁ : β a₁
⊢ a₁ = a₁ ∧ HEq b₁ b₁
[PROOFSTEP]
exact ⟨rfl, heq_of_eq rfl⟩
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
x✝ : a₁ = a₂ ∧ HEq b₁ b₂
h₁ : a₁ = a₂
h₂ : HEq b₁ b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
[PROOFSTEP]
subst h₁
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ : α
b₁ b₂ : β a₁
x✝ : a₁ = a₁ ∧ HEq b₁ b₂
h₂ : HEq b₁ b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
[PROOFSTEP]
rw [eq_of_heq h₂]
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₀ x₁ : Sigma β
h₀ : x₀.fst = x₁.fst
h₁ : HEq x₀.snd x₁.snd
⊢ x₀ = x₁
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₁ : Sigma β
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝, snd := snd✝ }.fst = x₁.fst
h₁ : HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
⊢ { fst := fst✝, snd := snd✝ } = x₁
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₁ : HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₀
[GOAL]
case mk.mk.refl
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝ : α
snd✝¹ snd✝ : β fst✝
h₁ : HEq { fst := fst✝, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₁
[GOAL]
case mk.mk.refl.refl
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₀ x₁ : Sigma β
⊢ x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₁ : Sigma β
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = x₁ ↔
    { fst := fst✝, snd := snd✝ }.fst = x₁.fst ∧ HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ } ↔
    { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst ∧
      HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
[PROOFSTEP]
exact Sigma.mk.inj_iff
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
⊢ a = b ∧ HEq f g
[PROOFSTEP]
rcases‹Nonempty γ› with ⟨i⟩
[GOAL]
case intro
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
i : γ
⊢ a = b ∧ HEq f g
[PROOFSTEP]
obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)
[GOAL]
case intro
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ a = a ∧ HEq f g
[PROOFSTEP]
simpa [Function.funext_iff] using h
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h : Sigma.map f₁ f₂ { fst := i, snd := x } = Sigma.map f₁ f₂ { fst := j, snd := y }
⊢ { fst := i, snd := x } = { fst := j, snd := y }
[PROOFSTEP]
obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h : Sigma.map f₁ f₂ { fst := i, snd := x } = Sigma.map f₁ f₂ { fst := i, snd := y }
⊢ { fst := i, snd := x } = { fst := i, snd := y }
[PROOFSTEP]
obtain rfl : x = y := h₂ i (sigma_mk_injective h)
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
h : Sigma.map f₁ f₂ { fst := i, snd := x } = Sigma.map f₁ f₂ { fst := i, snd := x }
⊢ { fst := i, snd := x } = { fst := i, snd := x }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map f₁ f₂)
[PROOFSTEP]
simp only [Function.Surjective, Sigma.forall, h₁.forall]
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = { fst := f₁ x, snd := b }
[PROOFSTEP]
exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩
[GOAL]
α : Sort u_1
β : α → Sort u_2
x₀ x₁ : PSigma β
h₀ : x₀.fst = x₁.fst
h₁ : HEq x₀.snd x₁.snd
⊢ x₀ = x₁
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Sort u_1
β : α → Sort u_2
x₁ : PSigma β
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝, snd := snd✝ }.fst = x₁.fst
h₁ : HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
⊢ { fst := fst✝, snd := snd✝ } = x₁
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Sort u_1
β : α → Sort u_2
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₁ : HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₀
[GOAL]
case mk.mk.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝¹ snd✝ : β fst✝
h₁ : HEq { fst := fst✝, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₁
[GOAL]
case mk.mk.refl.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
β : α → Sort u_2
x₀ x₁ : PSigma β
⊢ x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Sort u_1
β : α → Sort u_2
x₁ : PSigma β
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = x₁ ↔
    { fst := fst✝, snd := snd✝ }.fst = x₁.fst ∧ HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Sort u_1
β : α → Sort u_2
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ } ↔
    { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst ∧
      HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
[PROOFSTEP]
exact PSigma.mk.inj_iff


[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b ↔ ∃ h, h ▸ a.snd ≤ b.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd
[PROOFSTEP]
rintro ⟨i, a, b, h⟩
[GOAL]
case mp.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ h, h ▸ { fst := i, snd := a }.snd ≤ { fst := i, snd := b }.snd
[PROOFSTEP]
exact ⟨rfl, h⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
case mpr.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ { fst := i, snd := a }.snd ≤ b.snd) → { fst := i, snd := a } ≤ b
[PROOFSTEP]
obtain ⟨j, b⟩ := b
[GOAL]
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
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 }
[PROOFSTEP]
rintro ⟨rfl : i = j, h⟩
[GOAL]
case mpr.mk.mk.intro
ι : Type u_1
α : ι → Type u_2
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 }
[PROOFSTEP]
exact le.fiber _ _ _ h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b ↔ ∃ h, h ▸ a.snd < b.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b → ∃ h, h ▸ a.snd < b.snd
[PROOFSTEP]
rintro ⟨i, a, b, h⟩
[GOAL]
case mp.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ h, h ▸ { fst := i, snd := a }.snd < { fst := i, snd := b }.snd
[PROOFSTEP]
exact ⟨rfl, h⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd < b.snd) → a < b
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
case mpr.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ { fst := i, snd := a }.snd < b.snd) → { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨j, b⟩ := b
[GOAL]
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α 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 }
[PROOFSTEP]
rintro ⟨rfl : i = j, h⟩
[GOAL]
case mpr.mk.mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α 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 }
[PROOFSTEP]
exact lt.fiber _ _ _ h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
⊢ ∀ (a b c : (i : ι) × α i), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
rintro _ _ _ ⟨i, a, b, hab⟩ ⟨_, _, c, hbc⟩
[GOAL]
case fiber.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
i : ι
a b : α i
hab : a ≤ b
c : α i
hbc : b ≤ c
⊢ { fst := i, snd := a } ≤ { fst := i, snd := c }
[PROOFSTEP]
exact le.fiber i a c (hab.trans hbc)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ < x✝ ↔ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ < x✝ → x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹
[PROOFSTEP]
rintro ⟨i, a, b, hab⟩
[GOAL]
case mp.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
i : ι
a b : α i
hab : a < b
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b } ∧ ¬{ fst := i, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_le]
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹ → x✝¹ < x✝
[PROOFSTEP]
rintro ⟨⟨i, a, b, hab⟩, h⟩
[GOAL]
case mpr.intro.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
i : ι
a b : α i
hab : a ≤ b
h : ¬{ fst := i, snd := b } ≤ { fst := i, snd := a }
⊢ { fst := i, snd := a } < { fst := i, snd := b }
[PROOFSTEP]
rw [mk_le_mk_iff] at h
[GOAL]
case mpr.intro.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE ((i : ι) × α i) := Sigma.LE
src✝ : LT ((i : ι) × α i) := Sigma.LT
i : ι
a b : α i
hab : a ≤ b
h : ¬b ≤ a
⊢ { fst := i, snd := a } < { fst := i, snd := b }
[PROOFSTEP]
exact mk_lt_mk_iff.2 (hab.lt_of_not_le h)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder ((i : ι) × α i) := Sigma.preorder
⊢ ∀ (a b : (i : ι) × α i), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
rintro _ _ ⟨i, a, b, hab⟩ ⟨_, _, _, hba⟩
[GOAL]
case fiber.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder ((i : ι) × α i) := Sigma.preorder
i : ι
a b : (fun i => α i) i
hab : a ≤ b
hba : b ≤ a
⊢ { fst := i, snd := a } = { fst := i, snd := b }
[PROOFSTEP]
exact ext rfl (heq_of_eq <| hab.antisymm hba)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : (i : ι) × α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨_, _⟩ ⟨_, _, b, h⟩
[GOAL]
case mk.mk.fiber
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.fiber.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, lt.fiber i a c ha, lt.fiber i c b hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
⊢ ∀ (a b : Σₗ (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
refine' fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, _⟩, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
a b : Σₗ (i : ι), α i
hab : a < b
⊢ ¬b ≤ a
[PROOFSTEP]
rintro (⟨b, a, hji⟩ | ⟨b, a, hba⟩)
[GOAL]
case refine'_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hab : { fst := j✝, snd := a } < { fst := i✝, snd := b }
⊢ False
[PROOFSTEP]
obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
[GOAL]
case refine'_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : { fst := i✝, snd := a } < { fst := i✝, snd := b }
⊢ False
[PROOFSTEP]
obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
[GOAL]
case refine'_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hij : j✝ < i✝
⊢ False
[PROOFSTEP]
exact hij.not_lt hji
[GOAL]
case refine'_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ : ι
b a : α i✝
hji : i✝ < i✝
hab : a < b
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hji
[GOAL]
case refine'_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ : ι
b a : α i✝
hba : b ≤ a
hij : i✝ < i✝
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hij
[GOAL]
case refine'_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : a < b
⊢ False
[PROOFSTEP]
exact hab.not_le hba
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
a b : Σₗ (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b
[PROOFSTEP]
rintro ⟨⟨a, b, hij⟩ | ⟨a, b, hab⟩, hba⟩
[GOAL]
case refine'_2.intro.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : i✝ < j✝
hba : ¬{ fst := j✝, snd := b } ≤ { fst := i✝, snd := a }
⊢ { fst := i✝, snd := a } < { fst := j✝, snd := b }
[PROOFSTEP]
exact Sigma.Lex.left _ _ hij
[GOAL]
case refine'_2.intro.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ (i : ι), α i) := Lex.LE
src✝ : LT (Σₗ (i : ι), α i) := Lex.LT
i✝ : ι
a b : α i✝
hab : a ≤ b
hba : ¬{ fst := i✝, snd := b } ≤ { fst := i✝, snd := a }
⊢ { fst := i✝, snd := a } < { fst := i✝, snd := b }
[PROOFSTEP]
exact Sigma.Lex.right _ _ (hab.lt_of_not_le fun h => hba <| Sigma.Lex.right _ _ h)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
⊢ ⊥ ≤ { fst := a, snd := b }
[PROOFSTEP]
obtain rfl | ha := eq_bot_or_bot_lt a
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ (i : ι), α i
b : α ⊥
⊢ ⊥ ≤ { fst := ⊥, snd := b }
[PROOFSTEP]
exact Lex.right _ _ bot_le
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ ⊥ ≤ { fst := a, snd := b }
[PROOFSTEP]
exact Lex.left _ _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
⊢ { fst := a, snd := b } ≤ ⊤
[PROOFSTEP]
obtain rfl | ha := eq_top_or_lt_top a
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
b : α ⊤
⊢ { fst := ⊤, snd := b } ≤ ⊤
[PROOFSTEP]
exact Lex.right _ _ le_top
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ { fst := a, snd := b } ≤ ⊤
[PROOFSTEP]
exact Lex.left _ _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : Σₗ (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | ⟨_, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨k, hi, hj⟩ := exists_between h
[GOAL]
case mk.mk.left.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c⟩ : Nonempty (α k) := inferInstance
[GOAL]
case mk.mk.left.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
c : α k
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | ⟨_, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c, ha⟩ := exists_gt a
[GOAL]
case mk.mk.left.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α i
ha : a < c
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ _ ha, left _ _ h⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | ⟨_, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c, hb⟩ := exists_lt b
[GOAL]
case mk.mk.left.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α j
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨j, c⟩, left _ _ h, right _ _ hb⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ ∀ (a : Σₗ (i : ι), α i), ∃ b, a < b
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨j, h⟩ := exists_gt i
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨b⟩ : Nonempty (α j) := inferInstance
[GOAL]
case mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
exact ⟨⟨j, b⟩, left _ _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ ∀ (a : Σₗ (i : ι), α i), ∃ b, b < a
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨j, h⟩ := exists_lt i
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨b⟩ : Nonempty (α j) := inferInstance
[GOAL]
case mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
exact ⟨⟨j, b⟩, left _ _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a : Σₗ (i : ι), α i), ∃ b, a < b
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨b, h⟩ := exists_gt a
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
exact ⟨⟨i, b⟩, right _ _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a : Σₗ (i : ι), α i), ∃ b, b < a
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨b, h⟩ := exists_lt a
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : b < a
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
exact ⟨⟨i, b⟩, right _ _ h⟩


[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
⊢ Countable (Π₀ (i : ι), α i)
[PROOFSTEP]
classical
let _ := Encodable.ofCountable ι
let _ := fun i ↦ Encodable.ofCountable (α i)
infer_instance
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
⊢ Countable (Π₀ (i : ι), α i)
[PROOFSTEP]
let _ := Encodable.ofCountable ι
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
x✝ : Encodable ι := Encodable.ofCountable ι
⊢ Countable (Π₀ (i : ι), α i)
[PROOFSTEP]
let _ := fun i ↦ Encodable.ofCountable (α i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
x✝¹ : Encodable ι := Encodable.ofCountable ι
x✝ : (i : ι) → Encodable (α i) := fun i => Encodable.ofCountable (α i)
⊢ Countable (Π₀ (i : ι), α i)
[PROOFSTEP]
infer_instance


[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Icc) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } ≤ { fst := k, snd := c } ∧ { fst := k, snd := c } ≤ { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, le_def, mem_Icc, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b) →
    ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
⊢ ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Ico) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } ≤ { fst := k, snd := c } ∧ { fst := k, snd := c } < { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ico, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b) →
    ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
⊢ ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Ioc) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } < { fst := k, snd := c } ∧ { fst := k, snd := c } ≤ { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ioc, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b) →
    ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
⊢ ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Ioo) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } < { fst := k, snd := c } ∧ { fst := k, snd := c } < { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, lt_def, mem_Ioo, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b) →
    ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
⊢ ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩