awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
obtain :
  ∀ (z : WithZero (Multiplicative ℤ)) (hz : z ≠ 0) (hzx : z ≤ x) (hzy : z ≤ y),
    ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y

Tactic:
obtain ⟨z, hz, hzx, hzy⟩ := WithZero.exists_ne_zero_and_le_and_le hx hy

Premises used: WithZero.exists_ne_zero_and_le_and_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
z : WithZero (Multiplicative ℤ)
hz : z ≠ 0
hzx : z ≤ x
hzy : z ≤ y
obtain : ∀ (k : ℕ) (hk : exp (-(↑k : ℤ)) < z), ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y

Tactic:
obtain ⟨k, hk⟩ := exists_exp_neg_natCast_lt hz

Premises used: WithZero.exists_exp_neg_natCast_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
z : WithZero (Multiplicative ℤ)
hz : z ≠ 0
hzx : z ≤ x
hzy : z ≤ y
k : ℕ
hk : exp (-(↑k : ℤ)) < z
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y

Tactic:
grind
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
zero : LE.le.{u_3} (α := WithZero (Multiplicative G)) 0 (exp (log 0))
coe : ∀ (a : Multiplicative G), (↑a : WithZero (Multiplicative G)) ≤ (↑a : WithZero (Multiplicative G))
⊢ x ≤ exp x.log

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
⊢ LE.le.{u_3} (α := WithZero (Multiplicative G)) 0 (exp (log 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
a : Multiplicative G
⊢ (↑a : WithZero (Multiplicative G)) ≤ (↑a : WithZero (Multiplicative G))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
s : Finset ι
a b : ι → M₀
inst_1 : SemilatticeSup M₀
inst_2 : OrderBot M₀
inst_3 : PosMulMono M₀
inst_4 : MulPosMono M₀
ha : ∀ i ∈ s, 0 ≤ a i
hb : ∀ i ∈ s, 0 ≤ b i
⊢ s.sup (a * b) ≤ s.sup a * s.sup b

Tactic:
Finset.sup_le fun _i hi ↦
    mul_le_mul (le_sup hi) (le_sup hi) (hb _ hi) ((ha _ hi).trans <| le_sup hi)

Premises used: Finset.sup_le, mul_le_mul, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
s : Finset ι
a b : ι → M₀
inst_1 : SemilatticeInf M₀
inst_2 : OrderTop M₀
inst_3 : PosMulMono M₀
inst_4 : MulPosMono M₀
ha : ∀ i ∈ s, 0 ≤ a i
hb : ∀ i ∈ s, 0 ≤ b i
⊢ s.inf a * s.inf b ≤ s.inf (a * b)

Tactic:
Finset.le_inf fun i hi ↦ mul_le_mul (inf_le hi) (inf_le hi) (Finset.le_inf hb) (ha i hi)

Premises used: mul_le_mul, Finset.le_inf, Finset.inf_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
s : Finset ι
a b : ι → M₀
inst_1 : SemilatticeSup M₀
inst_2 : PosMulMono M₀
inst_3 : MulPosMono M₀
ha : ∀ i ∈ s, 0 ≤ a i
hb : ∀ i ∈ s, 0 ≤ b i
hs : s.Nonempty
⊢ s.sup' hs (a * b) ≤ s.sup' hs a * s.sup' hs b

Tactic:
sup'_le _ _ fun _i hi ↦
    mul_le_mul (le_sup' _ hi) (le_sup' _ hi) (hb _ hi) ((ha _ hi).trans <| le_sup' _ hi)

Premises used: Finset.sup'_le, mul_le_mul, LE.le.trans, Finset.le_sup'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
s : Finset ι
a b : ι → M₀
inst_1 : SemilatticeInf M₀
inst_2 : PosMulMono M₀
inst_3 : MulPosMono M₀
ha : ∀ i ∈ s, 0 ≤ a i
hb : ∀ i ∈ s, 0 ≤ b i
hs : s.Nonempty
⊢ s.inf' hs a * s.inf' hs b ≤ s.inf' hs (a * b)

Tactic:
le_inf' _ _ fun _i hi ↦ mul_le_mul (inf'_le _ hi) (inf'_le _ hi) (le_inf' _ _ hb) (ha _ hi)

Premises used: mul_le_mul, Finset.le_inf', Finset.inf'_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
pos : ∀ (h : 0 = a), s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a
neg : ∀ (h : 0 ≠ a), s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a
⊢ s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a

Tactic:
by_cases! h : 0 = a
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 = a
⊢ s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 ≠ a
⊢ s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a

Tactic:
map_finset_sup' (OrderIso.mulRight₀ _ (lt_of_le_of_ne ha h)) hs f

Premises used: map_finset_sup', OrderIso.mulRight₀, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 ≠ a
⊢ s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a

Tactic:
exact map_finset_sup' (OrderIso.mulRight₀ _ (lt_of_le_of_ne ha h)) hs f

Premises used: map_finset_sup', OrderIso.mulRight₀, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
pos : ∀ (h : 0 = a), a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i
neg : ∀ (h : 0 ≠ a), a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i
⊢ a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i

Tactic:
by_cases! h : 0 = a
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 = a
⊢ a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 ≠ a
⊢ a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i

Tactic:
map_finset_sup' (OrderIso.mulLeft₀ _ (lt_of_le_of_ne ha h)) hs f

Premises used: map_finset_sup', OrderIso.mulLeft₀, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 ≠ a
⊢ a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i

Tactic:
exact map_finset_sup' (OrderIso.mulLeft₀ _ (lt_of_le_of_ne ha h)) hs f

Premises used: map_finset_sup', OrderIso.mulLeft₀, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
pos : ∀ (h : 0 = a), s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
neg : ∀ (h : 0 ≠ a), s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
⊢ s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a

Tactic:
by_cases! h : 0 = a
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 = a
⊢ s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 ≠ a
⊢ s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a

Tactic:
map_finset_sup' (OrderIso.divRight₀ _ (lt_of_le_of_ne ha h)) hs f

Premises used: map_finset_sup', OrderIso.divRight₀, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 ≠ a
⊢ s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a

Tactic:
exact map_finset_sup' (OrderIso.divRight₀ _ (lt_of_le_of_ne ha h)) hs f

Premises used: map_finset_sup', OrderIso.divRight₀, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
inl : sup ∅ f / a = sup ∅ fun (i : ι) ↦ f i / a
inr : ∀ (hs : s.Nonempty), s.sup f / a = s.sup fun (i : ι) ↦ f i / a
⊢ s.sup f / a = s.sup fun (i : ι) ↦ f i / a

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
f : ι → G₀
⊢ sup ∅ f / a = sup ∅ fun (i : ι) ↦ f i / a

Tactic:
simp [← show (0 : G₀) = ⊥ from bot_unique zero_le']

Premises used: zero_le', bot_unique
-- Module: Mathlib.Algebra.Order.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
inr : s.sup' hs f / a = s.sup fun (i : ι) ↦ f i / a
inr₁ : s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
inr₂ inr₃ : Eq.{u_3 + 1} (α := G₀) (s.sup' hs fun (i : ι) ↦ f i / a) (s.sup' hs fun (i : ι) ↦ f i / a)
⊢ s.sup f / a = s.sup fun (i : ι) ↦ f i / a

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]

Premises used: Finset.sup'_eq_sup, Finset.sup'_div₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
⊢ Monotone (α := M₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inl M₀ N₀) : (a : M₀) → WithZero (M₀ˣ × N₀ˣ))

Tactic:
(WithZero.map'_mono MonoidHom.inl_mono).comp ?_

Premises used: WithZero.map'_mono, Monotone.comp, MonoidHom.inl_mono, WithZero.recZeroCoe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
refine :
  Monotone (α := M₀) (β := WithZero M₀ˣ)
    (⇑(↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ)
⊢ Monotone (α := M₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inl M₀ N₀) : (a : M₀) → WithZero (M₀ˣ × N₀ˣ))

Tactic:
refine (WithZero.map'_mono MonoidHom.inl_mono).comp ?_

Premises used: WithZero.map'_mono, Monotone.comp, MonoidHom.inl_mono
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
x y : M₀
inl :
  0 ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
inr :
  ∀ (x : M₀ˣ),
    (↑x : M₀) ≤ y →
      LE.le (α := WithZero M₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
          WithZero M₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
          WithZero M₀ˣ)
⊢ x ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) x :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)

Tactic:
obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
y : M₀
inl :
  LE.le.{u_1} (α := M₀) 0 0 →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
inl₁ :
  ∀ (y : M₀ˣ),
    0 ≤ (↑y : M₀) →
      LE.le (α := WithZero M₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
          WithZero M₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑y : M₀) :
          WithZero M₀ˣ)
⊢ 0 ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
y : M₀
x : M₀ˣ
inr :
  (↑x : M₀) ≤ 0 →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
inr₁ :
  ∀ (y : M₀ˣ),
    (↑x : M₀) ≤ (↑y : M₀) →
      LE.le (α := WithZero M₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
          WithZero M₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑y : M₀) :
          WithZero M₀ˣ)
⊢ (↑x : M₀) ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
⊢ LE.le.{u_1} (α := M₀) 0 0 →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
y : M₀ˣ
⊢ 0 ≤ (↑y : M₀) →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑y : M₀) :
        WithZero M₀ˣ)

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
x : M₀ˣ
⊢ (↑x : M₀) ≤ 0 →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
x y : M₀ˣ
⊢ (↑x : M₀) ≤ (↑y : M₀) →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑y : M₀) :
        WithZero M₀ˣ)

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : PartialOrder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
⊢ StrictMono (α := M₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inl M₀ N₀) : (a : M₀) → WithZero (M₀ˣ × N₀ˣ))

Tactic:
inl_mono.strictMono_of_injective inl_injective

Premises used: MonoidWithZeroHom.inl_injective, Monotone.strictMono_of_injective
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
⊢ Monotone (α := N₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inr M₀ N₀) : (a : N₀) → WithZero (M₀ˣ × N₀ˣ))

Tactic:
(WithZero.map'_mono MonoidHom.inr_mono).comp ?_

Premises used: WithZero.map'_mono, MonoidHom.inr_mono, Monotone.comp, WithZero.recZeroCoe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
refine :
  Monotone (α := N₀) (β := WithZero N₀ˣ)
    (⇑(↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ)
⊢ Monotone (α := N₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inr M₀ N₀) : (a : N₀) → WithZero (M₀ˣ × N₀ˣ))

Tactic:
refine (WithZero.map'_mono MonoidHom.inr_mono).comp ?_

Premises used: WithZero.map'_mono, MonoidHom.inr_mono, Monotone.comp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
x y : N₀
inl :
  0 ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
inr :
  ∀ (x : N₀ˣ),
    (↑x : N₀) ≤ y →
      LE.le (α := WithZero N₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
          WithZero N₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
          WithZero N₀ˣ)
⊢ x ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) x :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)

Tactic:
obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
y : N₀
inl :
  LE.le.{u_2} (α := N₀) 0 0 →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
inl₁ :
  ∀ (y : N₀ˣ),
    0 ≤ (↑y : N₀) →
      LE.le (α := WithZero N₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
          WithZero N₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑y : N₀) :
          WithZero N₀ˣ)
⊢ 0 ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
y : N₀
x : N₀ˣ
inr :
  (↑x : N₀) ≤ 0 →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
inr₁ :
  ∀ (y : N₀ˣ),
    (↑x : N₀) ≤ (↑y : N₀) →
      LE.le (α := WithZero N₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
          WithZero N₀ˣ)
        (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑y : N₀) :
          WithZero N₀ˣ)
⊢ (↑x : N₀) ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
⊢ LE.le.{u_2} (α := N₀) 0 0 →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
y : N₀ˣ
⊢ 0 ≤ (↑y : N₀) →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑y : N₀) :
        WithZero N₀ˣ)

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv