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

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

Tactic:
rintro rfl

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

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
b : Y
n : ℕ
⊢ pred^[n] b = f (pred^[n] (EquivLike.inv f b))

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

Result:
no goals

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

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

Result:
no goals

Proof state:
case zero
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
b : Y
⊢ pred^[0] b = f (pred^[0] (EquivLike.inv f b))

Tactic:
simp

Result:
no goals

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

Tactic:
refine (exists_pred_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✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∀ (a_1 : ℕ), pred^[a_1] (EquivLike.inv f b) = EquivLike.inv f a → pred^[a_1] b = a

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

Tactic:
intro n

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

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

Tactic:
clear h

Result:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
b : Y
n : ℕ
⊢ pred^[n] b = f (pred^[n] (EquivLike.inv f b))

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

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✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (pred^[n] (EquivLike.inv f b)) = a → pred^[n] b = a