awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : c < a * b
a' : α
hc' : c / a < a'
ha' : a' < b
⊢ ∃ (b' : α), b' < b ∧ c < a * b'

Tactic:
exact ⟨a', ha', div_lt_iff_lt_mul'.1 hc'⟩
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : a * b < c
obtain : ∀ (a' : α) (ha' : a < a') (hc' : a' < c / b), ∃ (a' : α), a' > a ∧ a' * b < c
⊢ ∃ (a' : α), a' > a ∧ a' * b < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt.2 hc)

Premises used: Iff.mpr, lt_div_iff_mul_lt, exists_between
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : a * b < c
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ (a' : α), a' > a ∧ a' * b < c

Tactic:
⟨a', ha', lt_div_iff_mul_lt.1 hc'⟩

Premises used: lt_div_iff_mul_lt, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : a * b < c
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ (a' : α), a' > a ∧ a' * b < c

Tactic:
exact ⟨a', ha', lt_div_iff_mul_lt.1 hc'⟩
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : a * b < c
obtain : ∀ (a' : α) (ha' : b < a') (hc' : a' < c / a), ∃ (b' : α), b' > b ∧ a * b' < c
⊢ ∃ (b' : α), b' > b ∧ a * b' < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt'.2 hc)

Premises used: Iff.mpr, lt_div_iff_mul_lt', exists_between
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : a * b < c
a' : α
ha' : b < a'
hc' : a' < c / a
⊢ ∃ (b' : α), b' > b ∧ a * b' < c

Tactic:
⟨a', ha', lt_div_iff_mul_lt'.1 hc'⟩

Premises used: lt_div_iff_mul_lt', And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : a * b < c
a' : α
ha' : b < a'
hc' : a' < c / a
⊢ ∃ (b' : α), b' > b ∧ a * b' < c

Tactic:
exact ⟨a', ha', lt_div_iff_mul_lt'.1 hc'⟩
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
refine : ∀ (d : α) (hd : a * b < d), c ≤ d
⊢ c ≤ a * b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd : a * b < d
obtain : ∀ (a' : α) (ha' : a' > a) (hd : a' * b < d), c ≤ d
⊢ c ≤ d

Tactic:
obtain ⟨a', ha', hd⟩ := exists_mul_left_lt hd

Premises used: _private.0.exists_mul_left_lt
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
obtain : ∀ (b' : α) (hb' : b' > b) (hd : a' * b' < d), c ≤ d
⊢ c ≤ d

Tactic:
obtain ⟨b', hb', hd⟩ := exists_mul_right_lt hd

Premises used: _private.0.exists_mul_right_lt
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd_2 : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Tactic:
(h a' ha' b' hb').trans hd.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd_2 : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' ha' b' hb').trans hd.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
refine : ∀ (d : α) (hd : d < a * b), d ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd : d < a * b
obtain : ∀ (a' : α) (ha' : a' < a) (hd : d < a' * b), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd

Premises used: _private.0.exists_lt_mul_left
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd_1 : d < a * b
a' : α
ha' : a' < a
hd : d < a' * b
obtain : ∀ (b' : α) (hb' : b' < b) (hd : d < a' * b'), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd

Premises used: _private.0.exists_lt_mul_right
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd_1 : d < a * b
a' : α
ha' : a' < a
hd_2 : d < a' * b
b' : α
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Tactic:
hd.le.trans (h a' ha' b' hb')

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd_1 : d < a * b
a' : α
ha' : a' < a
hd_2 : d < a' * b
b' : α
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Tactic:
exact hd.le.trans (h a' ha' b' hb')

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
obtain : ∀ (y : M) (hy : 1 < y) (hyx : y < x), ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x

Tactic:
obtain ⟨y, hy, hyx⟩ := exists_between hx

Premises used: exists_between
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx : y < x
inl : ∀ (hyx : HPow.hPow (β := ℕ) y 2 ≤ x), ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
inr : ∀ (hxy : x ≤ HPow.hPow (β := ℕ) y 2), ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x

Tactic:
obtain hyx | hxy := le_total (y ^ 2) x

Premises used: le_total, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx_1 : y < x
hyx : HPow.hPow (β := ℕ) y 2 ≤ x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x

Tactic:
⟨y, hy, hyx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx_1 : y < x
hyx : HPow.hPow (β := ℕ) y 2 ≤ x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x

Tactic:
exact ⟨y, hy, hyx⟩
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx : y < x
hxy : x ≤ HPow.hPow (β := ℕ) y 2
inr :
  ∀ (z : M) (hz : 1 < z) (hx : 1 < y * z) (hyx : y < y * z) (hxy : y * z ≤ HPow.hPow (β := ℕ) y 2),
    ∃ (y_1 : M), 1 < y_1 ∧ HPow.hPow (β := ℕ) y_1 2 ≤ y * z
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x

Tactic:
obtain ⟨z, hz, rfl⟩ := exists_one_lt_mul_of_lt' hyx

Premises used: exists_one_lt_mul_of_lt', rfl
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
y : M
hy : 1 < y
z : M
hz : 1 < z
hx : 1 < y * z
hyx : y < y * z
hxy : y * z ≤ HPow.hPow (β := ℕ) y 2
⊢ HPow.hPow (β := ℕ) z 2 ≤ y * z

Tactic:
simpa [pow_succ] using hxy

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
y : M
hy : 1 < y
z : M
hz : 1 < z
hx : 1 < y * z
hyx : y < y * z
hxy : y * z ≤ HPow.hPow (β := ℕ) y 2
⊢ ∃ (y_1 : M), 1 < y_1 ∧ HPow.hPow (β := ℕ) y_1 2 ≤ y * z

Tactic:
exact ⟨z, hz, by simpa [pow_succ] using hxy⟩
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
⊢ 1 < x ∧ HPow.hPow (β := ℕ) x 0 < x

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 1 < x

Tactic:
simpa using exists_between hx

Premises used: exists_between
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
obtain : ∀ (y : M) (hy : 1 < y) (hyx : y ^ (n + 1) < x), ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x
⊢ ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x

Tactic:
obtain ⟨y, hy, hyx⟩ := exists_pow_lt_of_one_lt hx (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
obtain : ∀ (z : M) (hz : 1 < z) (hzy : HPow.hPow (β := ℕ) z 2 ≤ y), ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x
⊢ ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x

Tactic:
obtain ⟨z, hz, hzy⟩ := exists_pow_two_le_of_one_lt hy

Premises used: _private.0.exists_pow_two_le_of_one_lt
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
⊢ ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x

Tactic:
⟨z, hz, hyx.trans_le' ?_⟩

Premises used: LT.lt.trans_le', And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
refine : z ^ (n + 2) ≤ y ^ (n + 1)
⊢ ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x

Tactic:
refine ⟨z, hz, hyx.trans_le' ?_⟩
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
⊢ n + 2 ≤ 2 * (n + 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
rw rw₁ : HPow.hPow (β := ℕ) z 2 ^ (n + 1) = HPow.hPow (β := ℕ) z 2 ^ (n + 1)
⊢ z ^ (2 * (n + 1)) = HPow.hPow (β := ℕ) z 2 ^ (n + 1)

Tactic:
rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
⊢ HPow.hPow (β := ℕ) z 2 ^ (n + 1) ≤ y ^ (n + 1)

Tactic:
pow_le_pow_left' hzy (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
calc : z ^ (2 * (n + 1)) = HPow.hPow (β := ℕ) z 2 ^ (n + 1)
⊢ z ^ (n + 2) ≤ y ^ (n + 1)

Tactic:
calc z ^ (n + 2)
      _ ≤ z ^ (2 * (n + 1)) := pow_right_monotone hz.le (by lia)
      _ = (z ^ 2) ^ (n + 1) := by rw [pow_mul]
      _ ≤ y ^ (n + 1) := pow_le_pow_left' hzy (n + 1)

Premises used: HMul.hMul, LT.lt.le, pow_right_monotone, HPow.hPow, HAdd.hAdd, OfNat.ofNat, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommGroup M
inst_3 : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
obtain : ∀ (y : M) (hy : 1 < y) (hy' : y ^ n < x⁻¹), ∃ (y : M), y < 1 ∧ x < y ^ n
⊢ ∃ (y : M), y < 1 ∧ x < y ^ n

Tactic:
obtain ⟨y, hy, hy'⟩ := exists_pow_lt_of_one_lt (one_lt_inv_of_inv hx) n

Premises used: one_lt_inv_of_inv, exists_pow_lt_of_one_lt
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommGroup M
inst_3 : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
right : x < y⁻¹ ^ n
⊢ ∃ (y : M), y < 1 ∧ x < y ^ n

Tactic:
use y⁻¹, inv_lt_one_of_one_lt hy

Premises used: inv_lt_one_of_one_lt
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommGroup M
inst_3 : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
⊢ x < y⁻¹ ^ n

Tactic:
simpa [lt_inv'] using hy'

Premises used: lt_inv'
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
⊢ 1 = RelHom.id r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
f g : r →r r
⊢ f * g = f.comp (r := r) (s := r) (t := r) g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
⊢ Eq.{u_1 + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
f g : r →r r
⊢ Eq (α := (a : α) → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
a : α
⊢ (1 : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
e₁ e₂ : r →r r
x : α
⊢ Eq (α := α) ((e₁ * e₂ : (a : α) → α) x : α) ((e₁ : (a : α) → α) ((e₂ : (a : α) → α) x : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
⊢ 1 = RelEmbedding.refl r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
f g : r ↪r r
⊢ f * g = g.trans (r := r) (s := r) (t := r) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
f g : r ↪r r
⊢ Eq (α := (a : α) → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
e₁ e₂ : r ↪r r
x : α
⊢ Eq (α := α) ((e₁ * e₂ : (a : α) → α) x : α) ((e₁ : (a : α) → α) ((e₂ : (a : α) → α) x : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
⊢ 1 = RelIso.refl r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
f g : r ≃r r
⊢ f * g = g.trans (r := r) (s := r) (t := r) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
e₁ e₂ : r ≃r r
⊢ Eq (α := (a : α) → α) (⇑(e₁ * e₂) : (a : α) → α) (Function.comp (β := α) (⇑e₁ : (a : α) → α) (⇑e₂ : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
x : α
⊢ (1 : (a : α) → α) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
e₁ e₂ : r ≃r r
x : α
⊢ Eq (α := α) ((e₁ * e₂ : (a : α) → α) x : α) ((e₁ : (a : α) → α) ((e₂ : (a : α) → α) x : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
e : r ≃r r
x : α
⊢ (e⁻¹ : (a : α) → α) ((e : (a : α) → α) x : α) = x

Tactic:
e.symm_apply_apply x

Premises used: RelIso.symm_apply_apply
-- Module: Mathlib.Algebra.Order.Group.End
Goal:
α : Type u_1
r : α → α → Prop
e : r ≃r r
x : α
⊢ (e : (a : α) → α) ((e⁻¹ : (a : α) → α) x : α) = x

Tactic:
e.apply_symm_apply x

Premises used: RelIso.apply_symm_apply
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
x x_1 : α
⊢ Equiv.toFun toLex (x * x_1) = Equiv.toFun toLex x * Equiv.toFun toLex x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
x x_1 : Lex α
⊢ Equiv.toFun ofLex (x * x_1) = Equiv.toFun ofLex x * Equiv.toFun ofLex x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
⊢ Eq (α := (a : α) → Lex α) (⇑(toLexMulEquiv α) : (a : α) → Lex α) (⇑toLex : (a : α) → Lex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
⊢ Eq (α := (a : Lex α) → α) (⇑(ofLexMulEquiv α) : (a : Lex α) → α) (⇑ofLex : (a : Lex α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
⊢ Eq (α := Lex α ≃* α) (MulEquiv.symm (toLexMulEquiv α)) (ofLexMulEquiv α)

Tactic:
rfl

Premises used: ofLexMulEquiv, Lex, Equiv.symm, ofLex, MulEquiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
⊢ Eq (α := α ≃* Lex α) (MulEquiv.symm (ofLexMulEquiv α)) (toLexMulEquiv α)

Tactic:
rfl

Premises used: toLexMulEquiv, Lex, Equiv.symm, MulEquiv.symm, Equiv.refl, rfl, toLex
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
⊢ (↑(toLexMulEquiv α) : α ≃ Lex α) = toLex

Tactic:
rfl

Premises used: Lex, Equiv.refl, rfl, toLex
-- Module: Mathlib.Algebra.Order.Group.Equiv
Goal:
α : Type u_1
inst : Mul α
⊢ (↑(ofLexMulEquiv α) : Lex α ≃ α) = ofLex

Tactic:
rfl

Premises used: Lex, ofLex, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
h : Ne (α := ℕ) 0 0
⊢ (HSMul.hSMul (α := ℕ) 0 s).toFinset = s.toFinset

Tactic:
contradiction
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h : n + 1 ≠ 0
pos : ∀ (h : n = 0), ((n + 1) • s).toFinset = s.toFinset
neg : ∀ (h : ¬n = 0), ((n + 1) • s).toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
by_cases h : n = 0
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : n = 0
pos : (HAdd.hAdd (α := ℕ) 0 1 • s).toFinset = s.toFinset
pos₁ : (HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
pos₂ pos₃ : s.toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
rw [h, zero_add, one_nsmul]

Premises used: zero_add, one_nsmul
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : ¬n = 0
neg : (n • s + HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
neg₁ : (n • s).toFinset ∪ (HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
neg₂ : (n • s).toFinset ∪ s.toFinset = s.toFinset
neg₃ : s.toFinset ∪ s.toFinset = s.toFinset
neg₄ neg₅ : s.toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]

Premises used: Multiset.toFinset_add, Finset.union_idempotent, one_nsmul, add_nsmul
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}

Tactic:
⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩

Premises used: And.intro, Iff.intro, Multiset.ext'
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
refine_1 : ∀ (H : s.toFinset = {a}) (h : s.card = 0), False
refine_2 : ∀ (H : s.toFinset = {a}) (x : α), count x s = count x (HSMul.hSMul (β := Multiset α) s.card {a})
refine_3 : ∀ (H : s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}), s.toFinset = {a}
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}

Tactic:
refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
⊢ Eq (α := Finset α) ∅ {a}

Tactic:
rw [card_eq_zero.1 h, toFinset_zero] at H

Premises used: Multiset.card_eq_zero, Multiset.toFinset_zero, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
H₁ : Eq (α := Finset α) ∅ {a}
⊢ s.card = 0

Tactic:
rw [card_eq_zero.1 h, toFinset_zero] at H

Premises used: Multiset.card_eq_zero, Multiset.toFinset_zero, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : Eq (α := Finset α) ∅ {a}
h : s.card = 0
⊢ False

Tactic:
Finset.empty_ne_singleton _ H

Premises used: Finset.empty_ne_singleton
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : Eq (α := Finset α) ∅ {a}
h : s.card = 0
⊢ False

Tactic:
exact Finset.empty_ne_singleton _ H

Premises used: Finset.empty_ne_singleton