awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
⊢ Nonempty.{max 1 (u_1 + 1)} (Additive G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
exact LinearOrderedAddCommGroup.discrete_or_denselyOrdered (Additive G)

Premises used: Additive, LinearOrderedAddCommGroup.discrete_or_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
rw : Nonempty.{max 1 (u_1 + 1)} (Additive G ≃+o ℤ) ↔ ¬DenselyOrdered G
rw₁ : ¬DenselyOrdered.{u_1} (Additive G) ↔ ¬DenselyOrdered G
rw₂ rw₃ : ¬DenselyOrdered.{u_1} (Additive G) ↔ ¬DenselyOrdered.{u_1} (Additive G)
⊢ Nonempty.{max 1 (u_1 + 1)} (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Tactic:
rw [← OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr,
    LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered,
    denselyOrdered_iff_of_orderIsoClass e]

Premises used: LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered, denselyOrdered_iff_of_orderIsoClass, OrderAddMonoidIso.toMultiplicativeRight, Equiv.nonempty_congr
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
inst_4 : Nontrivial G
rw : ¬DenselyOrdered.{u_1} (Additive G) ↔ ¬DenselyOrdered G
⊢ IsCyclic G ↔ ¬DenselyOrdered G

Tactic:
rw [← isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered]

Premises used: LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered, isAddCyclic_additive_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
inst_4 : Nontrivial G
⊢ ¬DenselyOrdered.{u_1} (Additive G) ↔ ¬DenselyOrdered G

Tactic:
rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
rw : Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered.{u_2} Gˣ
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered G

Tactic:
rw [← denselyOrdered_units_iff]

Premises used: denselyOrdered_units_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered.{u_2} Gˣ

Tactic:
(LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp_left ?_

Premises used: Or.imp_left, Units, LinearOrderedCommGroup.discrete_or_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
refine : Nonempty.{u_2 + 1} (Gˣ ≃*o Multiplicative ℤ) → Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ))
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered.{u_2} Gˣ

Tactic:
refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp_left ?_

Premises used: Or.imp_left, Units, LinearOrderedCommGroup.discrete_or_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ))

Tactic:
⟨OrderMonoidIso.withZeroUnits.symm.trans f.withZero⟩

Premises used: OrderMonoidIso.withZero, Nonempty.intro, OrderMonoidIso.symm, OrderMonoidIso.trans, OrderMonoidIso.withZeroUnits, DFunLike.coe
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ))

Tactic:
exact ⟨OrderMonoidIso.withZeroUnits.symm.trans f.withZero⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
rw rw₁ rw₂ : Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered.{u_2} Gˣ
rw₃ : Nonempty.{u_2 + 1} (Gˣ ≃*o Multiplicative ℤ) → Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ))
rw₄ : ∀ (f : Gˣ ≃*o Multiplicative ℤ), Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ))
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered G

Tactic:
classical
  rw [← denselyOrdered_units_iff]
  refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp_left ?_
  intro ⟨f⟩
  exact ⟨OrderMonoidIso.withZeroUnits.symm.trans f.withZero⟩

Premises used: Or.imp_left, denselyOrdered_units_iff, Units, LinearOrderedCommGroup.discrete_or_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
rw : Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ↔ Nonempty.{u_2 + 1} (Gˣ ≃*o Multiplicative ℤ)
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬DenselyOrdered G

Tactic:
rw [← denselyOrdered_units_iff,
      ← LinearOrderedCommGroup.discrete_iff_not_denselyOrdered]

Premises used: denselyOrdered_units_iff, LinearOrderedCommGroup.discrete_iff_not_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ↔ Nonempty.{u_2 + 1} (Gˣ ≃*o Multiplicative ℤ)

Tactic:
Nonempty.congr ?_ ?_

Premises used: Nonempty.congr
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
refine_1 : (G ≃*o WithZero (Multiplicative ℤ)) → Gˣ ≃*o Multiplicative ℤ
refine_2 : (Gˣ ≃*o Multiplicative ℤ) → G ≃*o WithZero (Multiplicative ℤ)
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃*o WithZero (Multiplicative ℤ)) ↔ Nonempty.{u_2 + 1} (Gˣ ≃*o Multiplicative ℤ)

Tactic:
refine Nonempty.congr ?_ ?_

Premises used: Nonempty.congr
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
refine_1 :
  ∀ {a b : Gˣ},
    LE.le (α := Multiplicative ℤ)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((Equiv.symm MulEquiv.withZero : (a : WithZero Gˣ ≃* WithZero (Multiplicative ℤ)) → Gˣ ≃* Multiplicative ℤ)
              (MulEquiv.trans withZeroUnitsEquiv (↑f : G ≃* WithZero (Multiplicative ℤ)))))
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((Equiv.symm MulEquiv.withZero : (a : WithZero Gˣ ≃* WithZero (Multiplicative ℤ)) → Gˣ ≃* Multiplicative ℤ)
              (MulEquiv.trans withZeroUnitsEquiv (↑f : G ≃* WithZero (Multiplicative ℤ)))))
          b) ↔
      a ≤ b
⊢ Gˣ ≃*o Multiplicative ℤ

Tactic:
refine ⟨MulEquiv.withZero.symm (withZeroUnitsEquiv.trans f), ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
a b : Gˣ
refine_1 :
  unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G)) ⋯ ≤
      unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G)) ⋯ ↔
    a ≤ b
⊢ LE.le (α := Multiplicative ℤ)
      (Equiv.toFun
        (MulEquiv.toEquiv
          ((Equiv.symm MulEquiv.withZero : (a : WithZero Gˣ ≃* WithZero (Multiplicative ℤ)) → Gˣ ≃* Multiplicative ℤ)
            (MulEquiv.trans withZeroUnitsEquiv (↑f : G ≃* WithZero (Multiplicative ℤ)))))
        a)
      (Equiv.toFun
        (MulEquiv.toEquiv
          ((Equiv.symm MulEquiv.withZero : (a : WithZero Gˣ ≃* WithZero (Multiplicative ℤ)) → Gˣ ≃* Multiplicative ℤ)
            (MulEquiv.trans withZeroUnitsEquiv (↑f : G ≃* WithZero (Multiplicative ℤ)))))
        b) ↔
    a ≤ b

Tactic:
simp only [MulEquiv.withZero, withZeroUnitsEquiv, MulEquiv.trans_apply,
      MulEquiv.coe_mk, Equiv.coe_fn_mk, recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv,
      MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, map_eq_zero, coe_ne_zero,
      ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]

Premises used: WithZero.coe_ne_zero, WithZero.unzero_coe, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, Equiv.toFun_as_coe, OrderMonoidIso.coe_mulEquiv, WithZero.withZeroUnitsEquiv, MulEquiv.withZero, reduceDIte, map_eq_zero, MulEquiv.trans_apply, MulEquiv.coe_mk, MulEquiv.toEquiv_eq_coe, MulEquiv.symm_trans_apply, Equiv.coe_fn_mk, EquivLike.coe_coe, WithZero.recZeroCoe_coe
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
a b : Gˣ
refine_1 :
  unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G)) ⋯ ≤
      unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G)) ⋯ ↔
    (↑a : G) ≤ (↑b : G)
refine_1₁ :
  unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G)) ⋯ ≤
      unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G)) ⋯ ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G) : WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G) : WithZero (Multiplicative ℤ))
refine_1₂ :
  (↑(unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G)) ⋯) : WithZero (Multiplicative ℤ)) ≤
      (↑(unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G)) ⋯) : WithZero (Multiplicative ℤ)) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G) : WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G) : WithZero (Multiplicative ℤ))
refine_1₃ :
  (f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G) ≤
      (↑(unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G)) ⋯) : WithZero (Multiplicative ℤ)) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G) : WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G) : WithZero (Multiplicative ℤ))
refine_1₄ refine_1₅ :
  LE.le (α := WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G) : WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G) : WithZero (Multiplicative ℤ)) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G) : WithZero (Multiplicative ℤ))
      ((f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G) : WithZero (Multiplicative ℤ))
⊢ unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑a : G)) ⋯ ≤
      unzero (x := (f : (a : G) → WithZero (Multiplicative ℤ)) (↑b : G)) ⋯ ↔
    a ≤ b

Tactic:
rw [← Units.val_le_val, ← map_le_map_iff f, ← coe_le_coe, coe_unzero, coe_unzero]

Premises used: OrderIsoClass.map_le_map_iff, Units.val_le_val, WithZero.coe_unzero, WithZero.coe_le_coe
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
refine_2 :
  ∀ {a b : G},
    LE.le (α := WithZero (Multiplicative ℤ))
        (Equiv.toFun
          (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm withZeroUnitsEquiv)
              ((MulEquiv.withZero : (a : Gˣ ≃* Multiplicative ℤ) → WithZero Gˣ ≃* WithZero (Multiplicative ℤ))
                (↑f : Gˣ ≃* Multiplicative ℤ))))
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm withZeroUnitsEquiv)
              ((MulEquiv.withZero : (a : Gˣ ≃* Multiplicative ℤ) → WithZero Gˣ ≃* WithZero (Multiplicative ℤ))
                (↑f : Gˣ ≃* Multiplicative ℤ))))
          b) ↔
      a ≤ b
⊢ G ≃*o WithZero (Multiplicative ℤ)

Tactic:
refine ⟨withZeroUnitsEquiv.symm.trans (MulEquiv.withZero f), ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : G
refine_2 :
  LE.le (α := WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (if h : a = 0 then 0 else (↑(Units.mk0 a h) : WithZero Gˣ)) :
        WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (if h : b = 0 then 0 else (↑(Units.mk0 b h) : WithZero Gˣ)) :
        WithZero (Multiplicative ℤ)) ↔
    a ≤ b
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (Equiv.toFun
        (MulEquiv.toEquiv
          (MulEquiv.trans (MulEquiv.symm withZeroUnitsEquiv)
            ((MulEquiv.withZero : (a : Gˣ ≃* Multiplicative ℤ) → WithZero Gˣ ≃* WithZero (Multiplicative ℤ))
              (↑f : Gˣ ≃* Multiplicative ℤ))))
        a)
      (Equiv.toFun
        (MulEquiv.toEquiv
          (MulEquiv.trans (MulEquiv.symm withZeroUnitsEquiv)
            ((MulEquiv.withZero : (a : Gˣ ≃* Multiplicative ℤ) → WithZero Gˣ ≃* WithZero (Multiplicative ℤ))
              (↑f : Gˣ ≃* Multiplicative ℤ))))
        b) ↔
    a ≤ b

Tactic:
simp only [withZeroUnitsEquiv, MulEquiv.symm_mk, MulEquiv.withZero,
      MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
      MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]

Premises used: MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, Equiv.toFun_as_coe, WithZero.withZeroUnitsEquiv, MulEquiv.withZero, MulEquiv.trans_apply, MulEquiv.coe_mk, MulEquiv.toEquiv_eq_coe, Equiv.coe_fn_mk, EquivLike.coe_coe
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : G
h : a = 0
h_1 : b = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ)) ↔
    a ≤ b

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : G
h : a = 0
h_1 : ¬b = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (↑(Units.mk0 b h_1) : WithZero Gˣ) :
        WithZero (Multiplicative ℤ)) ↔
    a ≤ b

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : G
h : ¬a = 0
h_1 : b = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (↑(Units.mk0 a h) : WithZero Gˣ) :
        WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ)) ↔
    a ≤ b

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : G
h : ¬a = 0
h_1 : ¬b = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (↑(Units.mk0 a h) : WithZero Gˣ) :
        WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (↑(Units.mk0 b h_1) : WithZero Gˣ) :
        WithZero (Multiplicative ℤ)) ↔
    a ≤ b

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
rw : (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)

Tactic:
rw [← this]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2

Tactic:
⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩

Premises used: Set.WellFoundedOn.mono', HSub.hSub, Set.WellFoundedOn.mapsTo, HAdd.hAdd, Iff.intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
refine_1 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x + g) {x : G | 0 ≤ x} {x : G | g ≤ x}
refine_2 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : G),
    Membership.mem (γ := Set G) {x : G | 0 ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | 0 ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x + g) a b
refine_3 :
  ∀ (h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x - g) {x : G | g ≤ x} {x : G | 0 ≤ x}
refine_4 :
  ∀ (h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : G),
    Membership.mem (γ := Set G) {x : G | g ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | g ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x - g) a b
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2
refine_1 :
  ∀ ⦃x : G⦄,
    Membership.mem (γ := Set G) {x : G | 0 ≤ x} x →
      Membership.mem (γ := Set G) {x : G | g ≤ x} ((fun (x : G) ↦ x + g) x)
⊢ MapsTo (β := G) (fun (x : G) ↦ x + g) {x : G | 0 ≤ x} {x : G | g ≤ x}

Tactic:
try intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2
x : G
⊢ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x → Membership.mem (γ := Set G) {x : G | g ≤ x} ((fun (x : G) ↦ x + g) x)

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2
refine_2 :
  ∀ (a : G),
    Membership.mem (γ := Set G) {x : G | 0 ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | 0 ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x + g) a b
⊢ ∀ (a : G),
    Membership.mem (γ := Set G) {x : G | 0 ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | 0 ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x + g) a b

Tactic:
try intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2
a : G
⊢ Membership.mem (γ := Set G) {x : G | 0 ≤ x} a →
    ∀ (b : G),
      Membership.mem (γ := Set G) {x : G | 0 ≤ x} b →
        a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x + g) a b

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
refine_3 :
  ∀ ⦃x : G⦄,
    Membership.mem (γ := Set G) {x : G | g ≤ x} x →
      Membership.mem (γ := Set G) {x : G | 0 ≤ x} ((fun (x : G) ↦ x - g) x)
⊢ MapsTo (β := G) (fun (x : G) ↦ x - g) {x : G | g ≤ x} {x : G | 0 ≤ x}

Tactic:
try intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
x : G
⊢ Membership.mem (γ := Set G) {x : G | g ≤ x} x → Membership.mem (γ := Set G) {x : G | 0 ≤ x} ((fun (x : G) ↦ x - g) x)

Tactic:
simp [Function.onFun]

Premises used: Function.onFun