awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : SemilatticeInf M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
n : ℕ
⊢ (a ⊓ b) ^ n ≤ a ^ n ⊓ b ^ n

Tactic:
le_inf (pow_le_pow_left' inf_le_left _) (pow_le_pow_left' inf_le_right _)

Premises used: inf_le_right, le_inf, inf_le_left, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
x : M
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ x ^ n ↔ 1 ≤ x

Tactic:
⟨le_imp_le_of_lt_imp_lt fun h => pow_lt_one' h hn, fun h => one_le_pow_of_one_le' h n⟩

Premises used: one_le_pow_of_one_le', le_imp_le_of_lt_imp_lt, pow_lt_one', Iff.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n ≤ 1 ↔ x ≤ 1

Tactic:
one_le_pow_iff (M := Mᵒᵈ) hn

Premises used: one_le_pow_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
x : M
n : ℕ
hn : n ≠ 0
⊢ 1 < x ^ n ↔ 1 < x

Tactic:
lt_iff_lt_of_le_iff_le (pow_le_one_iff hn)

Premises used: pow_le_one_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n < 1 ↔ x < 1

Tactic:
lt_iff_lt_of_le_iff_le (one_le_pow_iff hn)

Premises used: one_le_pow_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
a : M
m n : ℕ
ha : 1 < a
⊢ a ^ m ≤ a ^ n ↔ m ≤ n

Tactic:
(pow_right_strictMono' ha).le_iff_le

Premises used: StrictMono.le_iff_le, pow_right_strictMono'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
a : M
m n : ℕ
ha : 1 < a
⊢ a ^ m < a ^ n ↔ m < n

Tactic:
(pow_right_strictMono' ha).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, pow_right_strictMono'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
n : ℕ
⊢ a ^ n < b ^ n → a < b

Tactic:
(pow_left_mono _).reflect_lt

Premises used: Monotone.reflect_lt, pow_left_mono
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b c : M
h : a * b < HPow.hPow (β := ℕ) c 2
⊢ min a b < c

Tactic:
simpa using min_lt_max_of_mul_lt_mul (h.trans_eq <| pow_two _)

Premises used: pow_two, LT.lt.trans_eq, min_lt_max_of_mul_lt_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b c : M
h : HPow.hPow (β := ℕ) a 2 < b * c
⊢ a < max b c

Tactic:
simpa using min_lt_max_of_mul_lt_mul ((pow_two _).symm.trans_lt h)

Premises used: pow_two, min_lt_max_of_mul_lt_mul, Eq.trans_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
inst_3 : MulRightStrictMono M
a b : M
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ b ^ n ↔ a ≤ b

Tactic:
(pow_left_strictMono hn).le_iff_le

Premises used: pow_left_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
inst_3 : MulRightStrictMono M
a b c : M
h : a * b ≤ HPow.hPow (β := ℕ) c 2
⊢ min a b ≤ c

Tactic:
simpa using min_le_max_of_mul_le_mul (h.trans_eq <| pow_two _)

Premises used: LE.le.trans_eq, pow_two, min_le_max_of_mul_le_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
inst_3 : MulRightStrictMono M
a b c : M
h : HPow.hPow (β := ℕ) a 2 ≤ b * c
⊢ a ≤ max b c

Tactic:
simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)

Premises used: pow_two, min_le_max_of_mul_le_mul, Eq.trans_le, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
n : ℕ
x : M
hn : 0 < n
⊢ x ^ n < 1 ↔ x < 1

Tactic:
haveI := mulLeftMono_of_mulLeftStrictMono M
  pow_lt_one_iff hn.ne'

Premises used: LT.lt.ne', pow_lt_one_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
n : ℕ
x : M
hn : 0 < n
⊢ x ^ n < 1 ↔ x < 1

Tactic:
Left.pow_lt_one_iff' hn

Premises used: Left.pow_lt_one_iff'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulRightStrictMono M
n : ℕ
x : M
hn : 0 < n
⊢ x ^ n < 1 ↔ x < 1

Tactic:
haveI := mulRightMono_of_mulRightStrictMono M
  ⟨fun H => not_le.mp fun k => H.not_ge <| Right.one_le_pow_of_le k, Right.pow_lt_one_of_lt hn⟩

Premises used: not_le, Right.one_le_pow_of_le, Right.pow_lt_one_of_lt, Iff.intro, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
H : 1 ≤ x
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ n

Tactic:
hn
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
H : 1 ≤ x
n : ℤ
hn : 0 ≤ n
lift : ∀ (n : ℕ), 1 ≤ HPow.hPow (β := ℤ) x (↑n : ℤ)
⊢ 1 ≤ x ^ n

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
rw : 1 ≤ x ^ n
⊢ 1 ≤ HPow.hPow (β := ℤ) x (↑n : ℤ)

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n

Tactic:
apply one_le_pow_of_one_le' H

Premises used: one_le_pow_of_one_le'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
hx : 1 < x
n : ℤ
hn : 0 < n
⊢ 0 ≤ n

Tactic:
Int.le_of_lt hn

Premises used: Int.le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
hx : 1 < x
n : ℤ
hn : 0 < n
lift : ∀ (n : ℕ) (hn : LT.lt (α := ℤ) 0 (↑n : ℤ)), 1 < HPow.hPow (β := ℤ) x (↑n : ℤ)
⊢ 1 < x ^ n

Tactic:
lift n to ℕ using Int.le_of_lt hn

Premises used: Int.le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
hx : 1 < x
n : ℕ
hn : LT.lt (α := ℤ) 0 (↑n : ℤ)
rw : 1 < x ^ n
⊢ 1 < HPow.hPow (β := ℤ) x (↑n : ℤ)

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
hx : 1 < x
n : ℕ
hn : LT.lt (α := ℤ) 0 (↑n : ℤ)
⊢ 1 < x ^ n

Tactic:
one_lt_pow' hx (Int.natCast_pos.mp hn).ne'

Premises used: one_lt_pow', LT.lt.ne', Iff.mp, Int.natCast_pos
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
hx : 1 < x
n : ℕ
hn : LT.lt (α := ℤ) 0 (↑n : ℤ)
⊢ 1 < x ^ n

Tactic:
exact one_lt_pow' hx (Int.natCast_pos.mp hn).ne'

Premises used: one_lt_pow', LT.lt.ne', Iff.mp, Int.natCast_pos
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : ExistsAddOfLE α
⊢ ExistsMulOfLE.{u_1} (Multiplicative α)

Tactic:
⟨@exists_add_of_le α _ _ _⟩

Premises used: ExistsMulOfLE.mk, ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
inst_2 : ExistsMulOfLE α
⊢ ExistsAddOfLE.{u_1} (Additive α)

Tactic:
⟨@exists_mul_of_le α _ _ _⟩

Premises used: ExistsAddOfLE.mk, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LE.le (α := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α)
      ((ofMul : (a : α) → Additive α) b : Additive α) ↔
    a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LT.lt (α := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α)
      ((ofMul : (a : α) → Additive α) b : Additive α) ↔
    a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : Additive α
⊢ LE.le (α := α) ((toMul : (a : Additive α) → α) a : α) ((toMul : (a : Additive α) → α) b : α) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : Additive α
⊢ LT.lt (α := α) ((toMul : (a : Additive α) → α) a : α) ((toMul : (a : Additive α) → α) b : α) ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
⊢ Eq.{u_1 + 1} (α := Additive α) ((ofMul : (a : α) → Additive α) ⊤ : Additive α) (⊤ : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
⊢ Eq.{u_1 + 1} (α := α) ((toMul : (a : Additive α) → α) ⊤ : α) (⊤ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
a : α
⊢ Eq (α := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α) (⊤ : Additive α) ↔ a = ⊤

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
a : Additive α
⊢ Eq (α := α) ((toMul : (a : Additive α) → α) a : α) (⊤ : α) ↔ a = ⊤

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
⊢ Eq.{u_1 + 1} (α := Additive α) ((ofMul : (a : α) → Additive α) ⊥ : Additive α) (⊥ : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
⊢ Eq.{u_1 + 1} (α := α) ((toMul : (a : Additive α) → α) ⊥ : α) (⊥ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
a : α
⊢ Eq (α := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α) (⊥ : Additive α) ↔ a = ⊥

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
a : Additive α
⊢ Eq (α := α) ((toMul : (a : Additive α) → α) a : α) (⊥ : α) ↔ a = ⊥

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LE.le (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α)
      ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α) ↔
    a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LT.lt (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α)
      ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α) ↔
    a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : Multiplicative α
⊢ LE.le (α := α) ((toAdd : (a : Multiplicative α) → α) a : α) ((toAdd : (a : Multiplicative α) → α) b : α) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : Preorder α
a b : Multiplicative α
⊢ LT.lt (α := α) ((toAdd : (a : Multiplicative α) → α) a : α) ((toAdd : (a : Multiplicative α) → α) b : α) ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
⊢ Eq.{u_1 + 1} (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) ⊤ : Multiplicative α)
    (⊤ : Multiplicative α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
⊢ Eq.{u_1 + 1} (α := α) ((toAdd : (a : Multiplicative α) → α) ⊤ : α) (⊤ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
a : α
⊢ Eq (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) (⊤ : Multiplicative α) ↔ a = ⊤

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
a : Multiplicative α
⊢ Eq (α := α) ((toAdd : (a : Multiplicative α) → α) a : α) (⊤ : α) ↔ a = ⊤

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
⊢ Eq.{u_1 + 1} (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) ⊥ : Multiplicative α)
    (⊥ : Multiplicative α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
⊢ Eq.{u_1 + 1} (α := α) ((toAdd : (a : Multiplicative α) → α) ⊥ : α) (⊥ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
a : α
⊢ Eq (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) (⊥ : Multiplicative α) ↔ a = ⊥

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
a : Multiplicative α
⊢ Eq (α := α) ((toAdd : (a : Multiplicative α) → α) a : α) (⊥ : α) ↔ a = ⊥

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
x x_1 : M
h : (↑u : M) * x ≤ (↑u : M) * x_1
⊢ x ≤ x_1

Tactic:
simpa using mul_le_mul_right h ↑u⁻¹

Premises used: Units.val, mul_le_mul_right, Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a b : M
⊢ (↑u : M) * a ≤ (↑u : M) * b ↔ a ≤ b

Tactic:
u.mulLECancellable_val.mul_le_mul_iff_left

Premises used: Units.mulLECancellable_val, MulLECancellable.mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a b : M
rw : (↑u : M) * ((↑u⁻¹ : M) * a) ≤ (↑u : M) * b ↔ a ≤ (↑u : M) * b
rw₁ rw₂ : a ≤ (↑u : M) * b ↔ a ≤ (↑u : M) * b
⊢ (↑u⁻¹ : M) * a ≤ b ↔ a ≤ (↑u : M) * b

Tactic:
rw [← u.mul_le_mul_iff_left, mul_inv_cancel_left]

Premises used: _private.0.Units.mul_le_mul_iff_left, Units.mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a b : M
rw : (↑u : M) * a ≤ (↑u : M) * ((↑u⁻¹ : M) * b) ↔ (↑u : M) * a ≤ b
rw₁ rw₂ : (↑u : M) * a ≤ b ↔ (↑u : M) * a ≤ b
⊢ a ≤ (↑u⁻¹ : M) * b ↔ (↑u : M) * a ≤ b

Tactic:
rw [← u.mul_le_mul_iff_left, mul_inv_cancel_left]

Premises used: _private.0.Units.mul_le_mul_iff_left, Units.mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
rw : (↑u : M) * 1 ≤ (↑u : M) * (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1
rw₁ : (↑u : M) ≤ (↑u : M) * (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1
rw₂ rw₃ : (↑u : M) ≤ 1 ↔ (↑u : M) ≤ 1
⊢ 1 ≤ (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1

Tactic:
rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]

Premises used: _private.0.Units.mul_le_mul_iff_left, Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
rw : (↑u : M) * (↑u⁻¹ : M) ≤ (↑u : M) * 1 ↔ 1 ≤ (↑u : M)
rw₁ : (↑u : M) * (↑u⁻¹ : M) ≤ (↑u : M) ↔ 1 ≤ (↑u : M)
rw₂ rw₃ : 1 ≤ (↑u : M) ↔ 1 ≤ (↑u : M)
⊢ (↑u⁻¹ : M) ≤ 1 ↔ 1 ≤ (↑u : M)

Tactic:
rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]

Premises used: _private.0.Units.mul_le_mul_iff_left, Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a : M
rw : (↑u : M) * 1 ≤ a ↔ (↑u : M) ≤ a
rw₁ rw₂ : (↑u : M) ≤ a ↔ (↑u : M) ≤ a
⊢ 1 ≤ (↑u⁻¹ : M) * a ↔ (↑u : M) ≤ a

Tactic:
rw [u.le_inv_mul_iff, mul_one]

Premises used: Units.le_inv_mul_iff, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a : M
rw : a ≤ (↑u : M) * 1 ↔ a ≤ (↑u : M)
rw₁ rw₂ : a ≤ (↑u : M) ↔ a ≤ (↑u : M)
⊢ (↑u⁻¹ : M) * a ≤ 1 ↔ a ≤ (↑u : M)

Tactic:
rw [u.inv_mul_le_iff, mul_one]

Premises used: Units.inv_mul_le_iff, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a b : M
u : Mˣ
rw : a * (↑u⁻¹ : M) * (↑u : M) ≤ b * (↑u : M) ↔ a ≤ b * (↑u : M)
rw₁ rw₂ : a ≤ b * (↑u : M) ↔ a ≤ b * (↑u : M)
⊢ a * (↑u⁻¹ : M) ≤ b ↔ a ≤ b * (↑u : M)

Tactic:
rw [← u.mul_le_mul_iff_right, u.inv_mul_cancel_right]

Premises used: _private.0.Units.mul_le_mul_iff_right, Units.inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a b : M
u : Mˣ
rw : a * (↑u : M) ≤ b * (↑u⁻¹ : M) * (↑u : M) ↔ a * (↑u : M) ≤ b
rw₁ rw₂ : a * (↑u : M) ≤ b ↔ a * (↑u : M) ≤ b
⊢ a ≤ b * (↑u⁻¹ : M) ↔ a * (↑u : M) ≤ b

Tactic:
rw [← u.mul_le_mul_iff_right, inv_mul_cancel_right]

Premises used: _private.0.Units.mul_le_mul_iff_right, Units.inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a : M
u : Mˣ
rw : 1 * (↑u : M) ≤ a ↔ (↑u : M) ≤ a
rw₁ rw₂ : (↑u : M) ≤ a ↔ (↑u : M) ≤ a
⊢ 1 ≤ a * (↑u⁻¹ : M) ↔ (↑u : M) ≤ a

Tactic:
rw [u.le_mul_inv_iff, one_mul]

Premises used: Units.le_mul_inv_iff, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a : M
u : Mˣ
rw : a ≤ 1 * (↑u : M) ↔ a ≤ (↑u : M)
rw₁ rw₂ : a ≤ (↑u : M) ↔ a ≤ (↑u : M)
⊢ a * (↑u⁻¹ : M) ≤ 1 ↔ a ≤ (↑u : M)

Tactic:
rw [u.mul_inv_le_iff, one_mul]

Premises used: Units.mul_inv_le_iff, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
a : M
ha : IsUnit a
⊢ MulLECancellable a

Tactic:
ha.unit.mulLECancellable_val

Premises used: IsUnit.unit, Units.mulLECancellable_val
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
a b c : M
ha : IsUnit a
⊢ a * b ≤ a * c ↔ b ≤ c

Tactic:
ha.unit.mul_le_mul_iff_left

Premises used: _private.0.Units.mul_le_mul_iff_left, IsUnit.unit
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a b c : M
hc : IsUnit c
⊢ a * c ≤ b * c ↔ a ≤ b

Tactic:
hc.unit.mul_le_mul_iff_right

Premises used: _private.0.Units.mul_le_mul_iff_right, IsUnit.unit
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := WithTop α) (↑1 : WithTop α) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
⊢ (↑a : WithTop α) = 1 ↔ a = 1

Tactic:
coe_eq_coe

Premises used: WithTop.coe_eq_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
⊢ (↑a : WithTop α) ≠ 1 ↔ a ≠ 1

Tactic:
coe_eq_one.ne

Premises used: WithTop.coe_eq_one, Iff.ne
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
⊢ 1 = (↑a : WithTop α) ↔ a = 1

Tactic:
eq_comm.trans coe_eq_one

Premises used: WithTop.coe_eq_one, eq_comm, Iff.trans
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Ne.{u + 1} (α := WithTop α) ⊤ 1

Tactic:
top_ne_coe

Premises used: WithTop.top_ne_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Ne.{u + 1} (α := WithTop α) 1 ⊤

Tactic:
coe_ne_top

Premises used: WithTop.coe_ne_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := α) (untop 1 ⋯) 1

Tactic:
rfl

Premises used: WithTop.untop, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
d : α
⊢ untopD d 1 = 1

Tactic:
rfl

Premises used: WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
inst_1 : LE α
a : α
⊢ 1 ≤ (↑a : WithTop α) ↔ 1 ≤ a

Tactic:
coe_le_coe

Premises used: WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
inst_1 : LE α
a : α
⊢ (↑a : WithTop α) ≤ 1 ↔ a ≤ 1

Tactic:
coe_le_coe

Premises used: WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
inst_1 : LT α
a : α
⊢ 1 < (↑a : WithTop α) ↔ 1 < a

Tactic:
coe_lt_coe

Premises used: WithTop.coe_lt_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
inst_1 : LT α
a : α
⊢ (↑a : WithTop α) < 1 ↔ a < 1

Tactic:
coe_lt_coe

Premises used: WithTop.coe_lt_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
β : Type u_1
f : α → β
⊢ map f 1 = (↑(f 1) : WithTop β)

Tactic:
rfl

Premises used: WithTop.map, WithTop.some, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
β : Type v
α : Type u_1
f : α → β
v : WithTop α
inst : One β
⊢ map f v = 1 ↔ ∃ (x : α), v = (↑x : WithTop α) ∧ f x = 1

Tactic:
map_eq_some_iff

Premises used: WithTop.map_eq_some_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
β : Type v
α : Type u_1
f : α → β
v : WithTop α
inst : One β
⊢ 1 = map f v ↔ ∃ (x : α), v = (↑x : WithTop α) ∧ f x = 1

Tactic:
some_eq_map_iff

Premises used: WithTop.some_eq_map_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : One α
a : α
inst_1 : Zero α
inst_2 : LE α
inst_3 : ZeroLEOneClass α
⊢ ZeroLEOneClass.{u} (WithTop α)

Tactic:
⟨coe_le_coe.2 zero_le_one⟩

Premises used: Iff.mpr, ZeroLEOneClass.mk, zero_le_one, WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a b : α
⊢ (↑(a + b) : WithTop α) = (↑a : WithTop α) + (↑b : WithTop α)

Tactic:
rfl

Premises used: WithTop.map₂, WithTop.some, rfl, Option.map₂
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x : WithTop α
⊢ ⊤ + x = ⊤

Tactic:
rfl

Premises used: WithTop.map₂, rfl, Option.map₂
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x : WithTop α
top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤
coe : ∀ (a : α), (↑a : WithTop α) + ⊤ = ⊤
⊢ x + ⊤ = ⊤

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
⊢ HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
⊢ (↑a : WithTop α) + ⊤ = ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithTop α
top : ⊤ + y = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ y = ⊤
coe : ∀ (a : α), (↑a : WithTop α) + y = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ y = ⊤
⊢ x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
cases x