-- Mathlib/GroupTheory/ArchimedeanDensely.lean
@[to_additive existing]
lemma LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
    {G : Type*} [LinearOrderedCommGroup G] [Nontrivial G] {g : G} :
    Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
let e : G ≃o Additive G := OrderIso.refl G

Result:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Proof state:
case refine_1
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : Additive G ≃+o ℤ
⊢ G ≃*o Multiplicative ℤ

Tactic:
exact ⟨AddEquiv.toMultiplicative' f, by simp⟩

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ Nonempty (Additive G ≃+o ℤ) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
refine Nonempty.congr (fun f ↦ ?_) (fun f ↦ ?_)

Result:
case refine_1
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : Additive G ≃+o ℤ
⊢ G ≃*o Multiplicative ℤ

case refine_2
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G ≃*o Multiplicative ℤ
⊢ Additive G ≃+o ℤ

Proof state:
case refine_2
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G ≃*o Multiplicative ℤ
⊢ Additive G ≃+o ℤ

Tactic:
exact ⟨MulEquiv.toAdditive' f, by simp⟩

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete]

Result:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ Nonempty (Additive G ≃+o ℤ) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G ≃*o Multiplicative ℤ
⊢ ∀ {a b : Additive G}, (MulEquiv.toAdditive' ↑f).toFun a ≤ (MulEquiv.toAdditive' ↑f).toFun b ↔ a ≤ b

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_,
  fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩ <;>
simp [Function.onFun]

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : Additive G ≃+o ℤ
⊢ ∀ {a b : G}, (AddEquiv.toMultiplicative' ↑f).toFun a ≤ (AddEquiv.toMultiplicative' ↑f).toFun b ↔ a ≤ b

Tactic:
simp

Result:
no goals