awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this :
  (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
rw :
  (WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
have rw₁ : Nonempty.{u_2 + 1} (Additive G ≃+o ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
Tactic: rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete,
      OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this :
  (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
rw :
  (WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
rw₁ : Nonempty.{u_2 + 1} (Additive G ≃+o ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
have rw₂ : Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
Tactic: rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete,
      OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
have suffices : (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
  WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
Tactic: suffices Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Set.WellFoundedOn {x | e g ≤ x} (· < ·) by
    rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete,
      OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
have refine_1 : ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : Additive G),
  Membership.mem (γ := Set (Additive G))
      (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) a →
    ∀ (b : Additive G),
      Membership.mem (γ := Set (Additive G))
          (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) b →
        a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (⇑e.symm : (a : Additive G) → G) a b
Tactic: refine ⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_,
    fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
refine_1 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : Additive G),
    Membership.mem (γ := Set (Additive G))
        (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) a →
      ∀ (b : Additive G),
        Membership.mem (γ := Set (Additive G))
            (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (⇑e.symm : (a : Additive G) → G) a b
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
have refine_2 : ∀ (h : WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2) (x : G),
  Membership.mem (γ := Set G) {x : G | g ≤ x} x →
    Membership.mem (α := Additive G) (γ := Set (Additive G)) {x : Additive G | (e : (a : G) → Additive G) g ≤ x}
      ((e : (a : G) → Additive G) x : Additive G)
Tactic: refine ⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_,
    fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
refine_1 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : Additive G),
    Membership.mem (γ := Set (Additive G))
        (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) a →
      ∀ (b : Additive G),
        Membership.mem (γ := Set (Additive G))
            (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (⇑e.symm : (a : Additive G) → G) a b
refine_2 :
  ∀ (h : WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2) (x : G),
    Membership.mem (γ := Set G) {x : G | g ≤ x} x →
      Membership.mem (α := Additive G) (γ := Set (Additive G)) {x : Additive G | (e : (a : G) → Additive G) g ≤ x}
        ((e : (a : G) → Additive G) x : Additive G)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
have refine_3 : ∀ (h : WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive 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 : Additive G) ↦ x1 < x2) (⇑e : (a : G) → Additive G) a b
Tactic: refine ⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_,
    fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
have rw : (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
Tactic: rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete (g := g⁻¹)]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_1 : ∀ (h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2),
  MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | g⁻¹ ≤ x} {x : G | x ≤ g}
Tactic: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
refine_1 :
  ∀ (h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2),
    MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | g⁻¹ ≤ x} {x : G | x ≤ g}
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_2 : ∀ (h : WellFoundedOn {x : G | x ≤ g} 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⁻¹) a b
Tactic: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
refine_1 :
  ∀ (h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2),
    MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | g⁻¹ ≤ x} {x : G | x ≤ g}
refine_2 :
  ∀ (h : WellFoundedOn {x : G | x ≤ g} 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⁻¹) a b
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_3 : ∀ (h : WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
  MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | x ≤ g} {x : G | g⁻¹ ≤ x}
Tactic: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
refine_1 :
  ∀ (h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2),
    MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | g⁻¹ ≤ x} {x : G | x ≤ g}
refine_2 :
  ∀ (h : WellFoundedOn {x : G | x ≤ g} 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⁻¹) a b
refine_3 :
  ∀ (h : WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | x ≤ g} {x : G | g⁻¹ ≤ x}
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_4 : ∀ (h : WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : G),
  Membership.mem (γ := Set G) {x : G | x ≤ g} a →
    ∀ (b : G),
      Membership.mem (γ := Set G) {x : G | x ≤ g} b →
        a > b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x⁻¹) a b
Tactic: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ 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 WithZero (Multiplicative ℤ))
have rw : Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
Tactic: rw [this, LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
⊢ Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
have refine_1 : (f : G₀ˣ ≃*o Multiplicative ℤ) → G₀ ≃* WithZero (Multiplicative ℤ)
Tactic: refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
refine_1 : (f : G₀ˣ ≃*o Multiplicative ℤ) → G₀ ≃* WithZero (Multiplicative ℤ)
⊢ Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
have refine_2 : ∀ (f : G₀ˣ ≃*o Multiplicative ℤ) {a b : G₀},
  (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    a ≤ b
Tactic: refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
refine_1 : (f : G₀ˣ ≃*o Multiplicative ℤ) → G₀ ≃* WithZero (Multiplicative ℤ)
refine_2 :
  ∀ (f : G₀ˣ ≃*o Multiplicative ℤ) {a b : G₀},
    (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          a ≤
        (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          b ↔
      a ≤ b
⊢ Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
have refine_3 : (f : G₀ ≃*o WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ
Tactic: refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
refine_1 : (f : G₀ˣ ≃*o Multiplicative ℤ) → G₀ ≃* WithZero (Multiplicative ℤ)
refine_2 :
  ∀ (f : G₀ˣ ≃*o Multiplicative ℤ) {a b : G₀},
    (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          a ≤
        (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          b ↔
      a ≤ b
refine_3 : (f : G₀ ≃*o WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ
⊢ Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
have refine_4 : ∀ (f : G₀ ≃*o WithZero (Multiplicative ℤ)) {a b : G₀ˣ},
  LE.le (α := Multiplicative ℤ)
      (Equiv.toFun
        (MulEquiv.toEquiv
          ((Equiv.symm MulEquiv.withZero : (a : WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ)
            (MulEquiv.trans WithZero.withZeroUnitsEquiv (↑f : G₀ ≃* WithZero (Multiplicative ℤ)))))
        a)
      (Equiv.toFun
        (MulEquiv.toEquiv
          ((Equiv.symm MulEquiv.withZero : (a : WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ)
            (MulEquiv.trans WithZero.withZeroUnitsEquiv (↑f : G₀ ≃* WithZero (Multiplicative ℤ)))))
        b) ↔
    a ≤ b
Tactic: refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
⊢ (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    a ≤ b
have refine_2 : (MulEquiv.toEquiv
          (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
            (↑((OrderMonoidIso.withZero : (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                    f :
                  WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
              WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
      0 ≤
    (MulEquiv.toEquiv
          (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
            (↑((OrderMonoidIso.withZero : (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                    f :
                  WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
              WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
      b ↔
  0 ≤ b
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
refine_2 :
  (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        0 ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    0 ≤ b
⊢ (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    a ≤ b
have refine_2₁ : ∀ (ha : a ≠ 0),
  (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    a ≤ b
Tactic: rcases eq_or_ne a 0 with rfl | ha