case h
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a ↔ x✝ ∈ Iio a ∩ range Rat.cast
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a : α
⊢ cutMap α a = Iio a ∩ range Rat.cast
ext
case h.mp
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a → x✝ ∈ Iio a ∩ range Rat.cast

case h.mpr
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ Iio a ∩ range Rat.cast → x✝ ∈ cutMap α a
case h
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a ↔ x✝ ∈ Iio a ∩ range Rat.cast
constructor
case h.mp.intro.intro
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : q ∈ {t | ↑t < a}
⊢ ↑q ∈ Iio a ∩ range Rat.cast
case h.mp
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a → x✝ ∈ Iio a ∩ range Rat.cast
rintro ⟨q, h, rfl⟩
no goals
case h.mp.intro.intro
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : q ∈ {t | ↑t < a}
⊢ ↑q ∈ Iio a ∩ range Rat.cast
exact ⟨h, q, rfl⟩
case h.mpr.intro.intro
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : ↑q ∈ Iio a
⊢ ↑q ∈ cutMap α a
case h.mpr
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ Iio a ∩ range Rat.cast → x✝ ∈ cutMap α a
rintro ⟨h, q, rfl⟩
no goals
case h.mpr.intro.intro
F : Type ?u.9231
α : Type u_1
β : Type ?u.9237
γ : Type ?u.9240
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : ↑q ∈ Iio a
⊢ ↑q ∈ cutMap α a
exact ⟨q, h, rfl⟩