-- Mathlib/Order/Hom/Basic.lean
lemma denselyOrdered_iff_of_orderIsoClass {X Y F : Type*} [Preorder X] [Preorder Y]
    [EquivLike F X Y] [OrderIsoClass F X Y] (f : F) :
    DenselyOrdered X ↔ DenselyOrdered Y

Proof state:
case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered Y → DenselyOrdered X

Tactic:
intro H

Result:
case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
⊢ DenselyOrdered X

Proof state:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hc⟩ := exists_between ((map_inv_lt_map_inv_iff f).mpr h)

Result:
case mp.intro
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
c : X
hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Proof state:
case mp.intro
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
c : X
hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨f c, by simpa using hc⟩

Result:
no goals

Proof state:
case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)

Result:
case mpr.intro
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
c : Y
hc : f a < c ∧ c < f b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Proof state:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered X → DenselyOrdered Y

Tactic:
intro H

Result:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
⊢ DenselyOrdered Y

Proof state:
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
c : Y
hc : f a < c ∧ c < f b
⊢ a < EquivLike.inv f c ∧ EquivLike.inv f c < b

Tactic:
simpa using hc

Result:
no goals

Proof state:
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
constructor

Result:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered X → DenselyOrdered Y

case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered Y → DenselyOrdered X

Proof state:
case mpr.intro
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
c : Y
hc : f a < c ∧ c < f b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨EquivLike.inv f c, by simpa using hc⟩

Result:
no goals

Proof state:
case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
⊢ DenselyOrdered X

Tactic:
refine ⟨fun a b h ↦ ?_⟩

Result:
case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Proof state:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
⊢ DenselyOrdered Y

Tactic:
refine ⟨fun a b h ↦ ?_⟩

Result:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Proof state:
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
c : X
hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b
⊢ a < f c ∧ f c < b

Tactic:
simpa using hc

Result:
no goals