-- Mathlib/Order/SuccPred/Archimedean.lean
/-- `IsSuccArchimedean` transfers across equivalences between `SuccOrder`s. -/
protected lemma IsSuccArchimedean.of_orderIso [SuccOrder X] [IsSuccArchimedean X] [SuccOrder Y]
    (f : X ≃o Y) : IsSuccArchimedean Y where
  exists_succ_iterate_of_le {a b} h

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∀ (a_1 : ℕ), succ^[a_1] (EquivLike.inv f a) = EquivLike.inv f b → succ^[a_1] a = b

Tactic:
intro n

Result:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ succ^[n] (EquivLike.inv f a) = EquivLike.inv f b → succ^[n] a = b

Proof state:
case zero
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
⊢ succ^[0] a = f (succ^[0] (EquivLike.inv f a))

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (succ^[n] (EquivLike.inv f a)) = b → succ^[n] a = b

Tactic:
rintro rfl

Result:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
h : a ≤ f (succ^[n] (EquivLike.inv f a))
⊢ succ^[n] a = f (succ^[n] (EquivLike.inv f a))

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ n, succ^[n] a = b

Tactic:
refine (exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_

Result:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∀ (a_1 : ℕ), succ^[a_1] (EquivLike.inv f a) = EquivLike.inv f b → succ^[a_1] a = b

Proof state:
case succ
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
n : ℕ
IH : ∀ {a : Y}, succ^[n] a = f (succ^[n] (EquivLike.inv f a))
a : Y
⊢ succ^[n + 1] a = f (succ^[n + 1] (EquivLike.inv f a))

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ succ^[n] (EquivLike.inv f a) = EquivLike.inv f b → succ^[n] a = b

Tactic:
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]

Result:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (succ^[n] (EquivLike.inv f a)) = b → succ^[n] a = b

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
⊢ succ^[n] a = f (succ^[n] (EquivLike.inv f a))

Tactic:
induction n generalizing a with
| zero => simp
| succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
h : a ≤ f (succ^[n] (EquivLike.inv f a))
⊢ succ^[n] a = f (succ^[n] (EquivLike.inv f a))

Tactic:
clear h

Result:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
⊢ succ^[n] a = f (succ^[n] (EquivLike.inv f a))