awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
rw : b ^ n * (a * a) = b ^ n * HPow.hPow (β := ℕ) a 2
⊢ b ^ n * a * a = b ^ n * HPow.hPow (β := ℕ) a 2
have rw₁ : b ^ n * (a * a) = b ^ n * (a * a)
Tactic: rw [mul_assoc, sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ b ^ n * HPow.hPow (β := ℕ) a 2 ≤ b ^ n * (b * a)
have grw : b ^ n * (b * a) ≤ b ^ n * (b * a)
Tactic: grw [hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ b ^ n * (b * a) = b ^ (n + 1) * a
have rw : b ^ n * b * a = b ^ (n + 1) * a
Tactic: rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
rw : b ^ n * b * a = b ^ (n + 1) * a
⊢ b ^ n * (b * a) = b ^ (n + 1) * a
have rw₁ : b ^ (n + 1) * a = b ^ (n + 1) * a
Tactic: rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a
have a₁ : a ^ (n + 2) = a ^ (n + 1) * a
Tactic: calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
a₁ : a ^ (n + 2) = a ^ (n + 1) * a
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a
have a₂ : a ^ (n + 1) * a ≤ b ^ n * a * a
Tactic: calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
a₁ : a ^ (n + 2) = a ^ (n + 1) * a
a₂ : a ^ (n + 1) * a ≤ b ^ n * a * a
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a
have a₃ : b ^ n * a * a = b ^ n * HPow.hPow (β := ℕ) a 2
Tactic: calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
a₁ : a ^ (n + 2) = a ^ (n + 1) * a
a₂ : a ^ (n + 1) * a ≤ b ^ n * a * a
a₃ : b ^ n * a * a = b ^ n * HPow.hPow (β := ℕ) a 2
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a
have a₄ : b ^ n * HPow.hPow (β := ℕ) a 2 ≤ b ^ n * (b * a)
Tactic: calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
a₁ : a ^ (n + 2) = a ^ (n + 1) * a
a₂ : a ^ (n + 1) * a ≤ b ^ n * a * a
a₃ : b ^ n * a * a = b ^ n * HPow.hPow (β := ℕ) a 2
a₄ : b ^ n * HPow.hPow (β := ℕ) a 2 ≤ b ^ n * (b * a)
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a
have a₅ : b ^ n * (b * a) = b ^ (n + 1) * a
Tactic: calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ (k + 1) ≤ b ^ (k + 1)
have rw : a ^ k * a ≤ b ^ k * b
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
β : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : Preorder β
inst_3 : MulLeftMono M
inst_4 : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone.{u_1, u_3} (β := M) fun (a : β) ↦ f a ^ (n + 1)
have simp_rw : Monotone.{u_1, u_3} (β := M) fun (a : β) ↦ f a ^ n * f a
Tactic: simp_rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
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
⊢ 1 ≤ x ^ n
have lift : ∀ (n : ℕ), 1 ≤ HPow.hPow (β := ℤ) x (↑n : ℤ)
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : Preorder G
inst_2 : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ HPow.hPow (β := ℤ) x (↑n : ℤ)
have rw : 1 ≤ x ^ n
Tactic: rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
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
⊢ 1 < x ^ n
have lift : ∀ (n : ℕ) (hn : LT.lt (α := ℤ) 0 (↑n : ℤ)), 1 < HPow.hPow (β := ℤ) x (↑n : ℤ)
Tactic: lift n to ℕ using Int.le_of_lt hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
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 < HPow.hPow (β := ℤ) x (↑n : ℤ)
have rw : 1 < x ^ n
Tactic: rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a b : M
⊢ (↑u⁻¹ : M) * a ≤ b ↔ a ≤ (↑u : M) * b
have rw : (↑u : M) * ((↑u⁻¹ : M) * a) ≤ (↑u : M) * b ↔ a ≤ (↑u : M) * b
Tactic: rw [← u.mul_le_mul_iff_left, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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
⊢ (↑u⁻¹ : M) * a ≤ b ↔ a ≤ (↑u : M) * b
have rw₁ : a ≤ (↑u : M) * b ↔ a ≤ (↑u : M) * b
Tactic: rw [← u.mul_le_mul_iff_left, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a b : M
⊢ a ≤ (↑u⁻¹ : M) * b ↔ (↑u : M) * a ≤ b
have rw : (↑u : M) * a ≤ (↑u : M) * ((↑u⁻¹ : M) * b) ↔ (↑u : M) * a ≤ b
Tactic: rw [← u.mul_le_mul_iff_left, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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
⊢ a ≤ (↑u⁻¹ : M) * b ↔ (↑u : M) * a ≤ b
have rw₁ : (↑u : M) * a ≤ b ↔ (↑u : M) * a ≤ b
Tactic: rw [← u.mul_le_mul_iff_left, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
⊢ 1 ≤ (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1
have rw : (↑u : M) * 1 ≤ (↑u : M) * (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1
Tactic: rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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
⊢ 1 ≤ (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1
have rw₁ : (↑u : M) ≤ (↑u : M) * (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1
Tactic: rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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
⊢ 1 ≤ (↑u⁻¹ : M) ↔ (↑u : M) ≤ 1
have rw₂ : (↑u : M) ≤ 1 ↔ (↑u : M) ≤ 1
Tactic: rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
⊢ (↑u⁻¹ : M) ≤ 1 ↔ 1 ≤ (↑u : M)
have rw : (↑u : M) * (↑u⁻¹ : M) ≤ (↑u : M) * 1 ↔ 1 ≤ (↑u : M)
Tactic: rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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)
⊢ (↑u⁻¹ : M) ≤ 1 ↔ 1 ≤ (↑u : M)
have rw₁ : (↑u : M) * (↑u⁻¹ : M) ≤ (↑u : M) ↔ 1 ≤ (↑u : M)
Tactic: rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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)
⊢ (↑u⁻¹ : M) ≤ 1 ↔ 1 ≤ (↑u : M)
have rw₂ : 1 ≤ (↑u : M) ↔ 1 ≤ (↑u : M)
Tactic: rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a : M
⊢ 1 ≤ (↑u⁻¹ : M) * a ↔ (↑u : M) ≤ a
have rw : (↑u : M) * 1 ≤ a ↔ (↑u : M) ≤ a
Tactic: rw [u.le_inv_mul_iff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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
⊢ 1 ≤ (↑u⁻¹ : M) * a ↔ (↑u : M) ≤ a
have rw₁ : (↑u : M) ≤ a ↔ (↑u : M) ≤ a
Tactic: rw [u.le_inv_mul_iff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulLeftMono M
u : Mˣ
a : M
⊢ (↑u⁻¹ : M) * a ≤ 1 ↔ a ≤ (↑u : M)
have rw : a ≤ (↑u : M) * 1 ↔ a ≤ (↑u : M)
Tactic: rw [u.inv_mul_le_iff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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)
⊢ (↑u⁻¹ : M) * a ≤ 1 ↔ a ≤ (↑u : M)
have rw₁ : a ≤ (↑u : M) ↔ a ≤ (↑u : M)
Tactic: rw [u.inv_mul_le_iff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a b : M
u : Mˣ
⊢ a * (↑u⁻¹ : M) ≤ b ↔ a ≤ b * (↑u : M)
have rw : a * (↑u⁻¹ : M) * (↑u : M) ≤ b * (↑u : M) ↔ a ≤ b * (↑u : M)
Tactic: rw [← u.mul_le_mul_iff_right, u.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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)
⊢ a * (↑u⁻¹ : M) ≤ b ↔ a ≤ b * (↑u : M)
have rw₁ : a ≤ b * (↑u : M) ↔ a ≤ b * (↑u : M)
Tactic: rw [← u.mul_le_mul_iff_right, u.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a b : M
u : Mˣ
⊢ a ≤ b * (↑u⁻¹ : M) ↔ a * (↑u : M) ≤ b
have rw : a * (↑u : M) ≤ b * (↑u⁻¹ : M) * (↑u : M) ↔ a * (↑u : M) ≤ b
Tactic: rw [← u.mul_le_mul_iff_right, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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
⊢ a ≤ b * (↑u⁻¹ : M) ↔ a * (↑u : M) ≤ b
have rw₁ : a * (↑u : M) ≤ b ↔ a * (↑u : M) ≤ b
Tactic: rw [← u.mul_le_mul_iff_right, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a : M
u : Mˣ
⊢ 1 ≤ a * (↑u⁻¹ : M) ↔ (↑u : M) ≤ a
have rw : 1 * (↑u : M) ≤ a ↔ (↑u : M) ≤ a
Tactic: rw [u.le_mul_inv_iff, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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
⊢ 1 ≤ a * (↑u⁻¹ : M) ↔ (↑u : M) ≤ a
have rw₁ : (↑u : M) ≤ a ↔ (↑u : M) ≤ a
Tactic: rw [u.le_mul_inv_iff, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : LE M
inst_2 : MulRightMono M
a : M
u : Mˣ
⊢ a * (↑u⁻¹ : M) ≤ 1 ↔ a ≤ (↑u : M)
have rw : a ≤ 1 * (↑u : M) ↔ a ≤ (↑u : M)
Tactic: rw [u.mul_inv_le_iff, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Units (goal)
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)
⊢ a * (↑u⁻¹ : M) ≤ 1 ↔ a ≤ (↑u : M)
have rw₁ : a ≤ (↑u : M) ↔ a ≤ (↑u : M)
Tactic: rw [u.mul_inv_le_iff, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x : WithTop α
⊢ x + ⊤ = ⊤
have top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x : WithTop α
top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤
⊢ x + ⊤ = ⊤
have coe : ∀ (a : α), (↑a : WithTop α) + ⊤ = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
⊢ x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤
have top : ⊤ + y = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ y = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
top : ⊤ + y = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ y = ⊤
⊢ x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤
have coe : ∀ (a : α), (↑a : WithTop α) + y = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ y = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
⊢ ⊤ + y = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ y = ⊤
have top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤
⊢ ⊤ + y = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ y = ⊤
have top₁ : ∀ (a : α), ⊤ + (↑a : WithTop α) = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ (↑a : WithTop α) = ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
a : α
⊢ (↑a : WithTop α) + y = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ y = ⊤
have coe : (↑a : WithTop α) + ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
a : α
coe : (↑a : WithTop α) + ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤
⊢ (↑a : WithTop α) + y = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ y = ⊤
have coe₁ : ∀ (a_1 : α), (↑a : WithTop α) + (↑a_1 : WithTop α) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ (↑a_1 : WithTop α) = ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
have top : ⊤ + y ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ y ≠ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
top : ⊤ + y ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
have coe : ∀ (a : α), (↑a : WithTop α) + y ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ y ≠ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
⊢ ⊤ + y ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ y ≠ ⊤
have top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ y ≠ ⊤
have top₁ : ∀ (a : α), ⊤ + (↑a : WithTop α) ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ (↑a : WithTop α) ≠ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
a : α
⊢ (↑a : WithTop α) + y ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ y ≠ ⊤
have coe : (↑a : WithTop α) + ⊤ ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
a : α
coe : (↑a : WithTop α) + ⊤ ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤
⊢ (↑a : WithTop α) + y ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ y ≠ ⊤
have coe₁ : ∀ (a_1 : α), (↑a : WithTop α) + (↑a_1 : WithTop α) ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ (↑a_1 : WithTop α) ≠ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : LT α
⊢ x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤
have simp_rw : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
Tactic: simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
a b c : α
⊢ (↑a : WithTop α) + (↑b : WithTop α) = (↑c : WithTop α) ↔
    ∃ (a' : α), ∃ (b' : α), (↑a' : WithTop α) = (↑a : WithTop α) ∧ (↑b' : WithTop α) = (↑b : WithTop α) ∧ a' + b' = c
have norm_cast : a + b = c ↔ ∃ (a' : α), ∃ (b' : α), a' = a ∧ b' = b ∧ a' + b' = c
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsRightCancelAdd α
hz : z ≠ ⊤
⊢ x + z = y + z ↔ x = y
have lift : ∀ (z : α), x + (↑z : WithTop α) = y + (↑z : WithTop α) ↔ x = y
Tactic: lift z to α using hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsLeftCancelAdd α
hx : x ≠ ⊤
⊢ x + y = x + z ↔ y = z
have lift : ∀ (x : α), (↑x : WithTop α) + y = (↑x : WithTop α) + z ↔ y = z
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x_1 y_1 z_1 : WithTop α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
x y z : WithTop α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) x y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) x z)
have top : (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x_1 y_1 z_1 : WithTop α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
x y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) x y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) x z)
have coe : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) z)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
y z : WithTop α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
have top : (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
have top₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a : WithTop α) z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
y z : WithTop α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z)
have coe : (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z)
Tactic: cases y
Cleared hypotheses: y