awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n ≠ 0 ∧ a ∈ s
refine_2 : ∀ (n : ℕ) (h : n.succ ≠ 0 ∧ a ∈ s), a ∈ n.succ • s
⊢ a ∈ n • s

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1

Premises used: And.left, Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
refine_2 : a ∈ n • s ∨ a ∈ s
⊢ a ∈ n.succ • s

Tactic:
rw [succ_nsmul, mem_add]

Premises used: Multiset.mem_add, succ_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s ∨ a ∈ s

Tactic:
Or.inr h.2

Premises used: And.right, Or.inr
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s ∨ a ∈ s

Tactic:
exact Or.inr h.2

Premises used: And.right, Or.inr
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ a ∈ n • s ↔ a ∈ s

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
s : Multiset α
n : ℕ
a : α
rw : n • ({a} + s) = HSMul.hSMul (β := Multiset α) n {a} + n • s
rw₁ rw₂ : HSMul.hSMul (β := Multiset α) n {a} + n • s = HSMul.hSMul (β := Multiset α) n {a} + n • s
⊢ n • (a ::ₘ s) = HSMul.hSMul (β := Multiset α) n {a} + n • s

Tactic:
rw [← singleton_add, nsmul_add]

Premises used: Multiset.singleton_add, nsmul_add
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
s : Multiset α
n : ℕ
⊢ (n • s).card = n * s.card

Tactic:
cardHom.map_nsmul ..

Premises used: AddMonoidHom.map_nsmul, Multiset.cardHom, Multiset.card
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
n m : ℕ
⊢ n • replicate m a = replicate (n * m) a

Tactic:
((replicateAddMonoidHom a).map_nsmul _ _).symm

Premises used: AddMonoidHom.map_nsmul, Multiset.ofList, Multiset.replicate, Eq.symm, Multiset.replicateAddMonoidHom
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
n : ℕ
rw : n • replicate 1 a = replicate n a
rw₁ : replicate (n * 1) a = replicate n a
rw₂ rw₃ : replicate n a = replicate n a
⊢ HSMul.hSMul (β := Multiset α) n {a} = replicate n a

Tactic:
rw [← replicate_one, nsmul_replicate, mul_one]

Premises used: Multiset.nsmul_replicate, mul_one, Multiset.replicate_one
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ (⇑(mapAddMonoidHom f) : (a : Multiset α) → Multiset β) = map f

Tactic:
rfl

Premises used: Multiset.map, rfl
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
⊢ map f (n • s) = n • map f s

Tactic:
(mapAddMonoidHom f).map_nsmul _ _

Premises used: Multiset.map, AddMonoidHom.map_nsmul, Multiset.mapAddMonoidHom
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • s) = n • filter p s

Tactic:
s.induction_on ?_ ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
refine_1 : filter p (HSMul.hSMul (β := Multiset α) n 0) = n • filter p 0
refine_2 :
  ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
⊢ filter p (n • s) = n • filter p s

Tactic:
refine s.induction_on ?_ ?_
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (HSMul.hSMul (β := Multiset α) n 0) = n • filter p 0

Tactic:
simp only [filter_zero, nsmul_zero]

Premises used: nsmul_zero, Multiset.filter_zero
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
refine_2 :
  filter p (HSMul.hSMul (β := Multiset α) n {a}) + n • filter p ha =
    HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0) + n • filter p ha
⊢ filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)

Tactic:
rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]

Premises used: Multiset.filter_cons, Multiset.nsmul_cons, nsmul_add, Multiset.filter_add
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
refine_2 : filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0)
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) + n • filter p ha =
    HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0) + n • filter p ha

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
pos : ∀ (hp : p a), filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n {a}
neg : ∀ (hp : ¬p a), filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n 0
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0)

Tactic:
split_ifs with hp
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
pos : ∀ (a_1 : α), a_1 ∈ HSMul.hSMul (β := Multiset α) n {a} → p a_1
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n {a}

Tactic:
simp only [filter_eq_self, nsmul_zero, filter_eq_nil]

Premises used: Multiset.filter_eq_self, nsmul_zero, Multiset.filter_eq_nil
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
b : α
hb : b ∈ HSMul.hSMul (β := Multiset α) n {a}
pos pos₁ pos₂ pos₃ : p a
⊢ p b

Tactic:
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

Premises used: Multiset.mem_singleton, Iff.mp, Multiset.mem_of_mem_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
neg : ∀ (a_1 : α), a_1 ∈ HSMul.hSMul (β := Multiset α) n {a} → ¬p a_1
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n 0

Tactic:
simp only [filter_eq_self, nsmul_zero, filter_eq_nil]

Premises used: Multiset.filter_eq_self, nsmul_zero, Multiset.filter_eq_nil
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ HSMul.hSMul (β := Multiset α) n {a}
neg neg₁ neg₂ neg₃ : ¬p a
⊢ ¬p b

Tactic:
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

Premises used: Multiset.mem_singleton, Iff.mp, Multiset.mem_of_mem_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
zero : countP p (HSMul.hSMul (α := ℕ) 0 s) = 0 * countP p s
succ : ∀ (n : ℕ), countP p (n • s) = n * countP p s → countP p ((n + 1) • s) = (n + 1) * countP p s
⊢ countP p (n • s) = n * countP p s

Tactic:
induction n
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ countP p (HSMul.hSMul (α := ℕ) 0 s) = 0 * countP p s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Premises used: zero_nsmul, Nat.succ_mul, succ_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
h : countP p (n • s) = n * countP p s
⊢ countP p ((n + 1) • s) = (n + 1) * countP p s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Premises used: zero_nsmul, Nat.succ_mul, succ_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ (⇑(countPAddMonoidHom p) : (a : Multiset α) → ℕ) = countP p

Tactic:
rfl

Premises used: Multiset.countP, rfl
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : ∀ (a : α), count a (n • s).dedup = count a s.dedup
⊢ (n • s).dedup = s.dedup

Tactic:
ext a
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
pos : ∀ (h : a ∈ s), count a (n • s).dedup = count a s.dedup
neg : ∀ (h : ¬a ∈ s), count a (n • s).dedup = count a s.dedup
⊢ count a (n • s).dedup = count a s.dedup

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : a ∈ s
⊢ count a (n • s).dedup = count a s.dedup

Tactic:
simp [h, hn]
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : ¬a ∈ s
⊢ count a (n • s).dedup = count a s.dedup

Tactic:
simp [h, hn]
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
simp [← h.le_dedup_iff_le, hn]

Premises used: Multiset.Nodup.le_dedup_iff_le
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
classical simp [← h.le_dedup_iff_le, hn]
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ (⇑(countAddMonoidHom a) : (a : Multiset α) → ℕ) = count a

Tactic:
rfl

Premises used: Multiset.count, Multiset.countP, rfl
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
s : Multiset α
zero : count a (HSMul.hSMul (α := ℕ) 0 s) = 0 * count a s
succ : ∀ (n : ℕ), count a (n • s) = n * count a s → count a ((n + 1) • s) = (n + 1) * count a s
⊢ count a (n • s) = n * count a s

Tactic:
induction n
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ count a (HSMul.hSMul (α := ℕ) 0 s) = 0 * count a s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Premises used: zero_nsmul, Nat.succ_mul, succ_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
n : ℕ
h : count a (n • s) = n * count a s
⊢ count a ((n + 1) • s) = (n + 1) * count a s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Premises used: zero_nsmul, Nat.succ_mul, succ_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : AddZeroClass β
f g : AddMonoidHom.{u_1, u_2} (Multiset α) β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) {x} : β) ((g : (a : Multiset α) → β) {x} : β)
h₁ : ∀ (s : Multiset α), Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) s : β) ((g : (a : Multiset α) → β) s : β)
⊢ f = g

Tactic:
ext s
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : AddZeroClass β
f g : AddMonoidHom.{u_1, u_2} (Multiset α) β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) {x} : β) ((g : (a : Multiset α) → β) {x} : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) 0 : β) ((g : (a : Multiset α) → β) 0 : β)

Tactic:
simp only [_root_.map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : AddZeroClass β
f g : AddMonoidHom.{u_1, u_2} (Multiset α) β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) {x} : β) ((g : (a : Multiset α) → β) {x} : β)
a : α
s : Multiset α
ih : Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) s : β) ((g : (a : Multiset α) → β) s : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) (a ::ₘ s) : β) ((g : (a : Multiset α) → β) (a ::ₘ s) : β)

Tactic:
simp only [← singleton_add, _root_.map_add, ih, h]

Premises used: Multiset.singleton_add, map_add
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : AddZeroClass β
f g : AddMonoidHom.{u_1, u_2} (Multiset α) β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) {x} : β) ((g : (a : Multiset α) → β) {x} : β)
s : Multiset α
h₁ : Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) 0 : β) ((g : (a : Multiset α) → β) 0 : β)
h₂ :
  ∀ (a : α) (s : Multiset α)
    (ih : Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) s : β) ((g : (a : Multiset α) → β) s : β)),
    Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) (a ::ₘ s) : β) ((g : (a : Multiset α) → β) (a ::ₘ s) : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) s : β) ((g : (a : Multiset α) → β) s : β)

Tactic:
induction s using Multiset.induction_on with
  | empty => simp only [_root_.map_zero]
  | cons a s ih => simp only [← singleton_add, _root_.map_add, ih, h]

Premises used: Multiset.singleton_add, map_zero, map_add, Multiset.cons
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
rw : count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
⊢ count a s ≤ count a (HSMul.hSMul (α := ℕ) (fold max 0 (map (fun (a : α) ↦ count a s) s)) s.dedup)

Tactic:
rw [count_nsmul]

Premises used: Multiset.count_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
pos : ∀ (h : a ∈ s), count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
neg : ∀ (h : ¬a ∈ s), count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
pos : count a s ≤ HMul.hMul (α := ℕ) (fold max 0 (map (fun (a : α) ↦ count a s) s)) 1
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup

Tactic:
grw [← one_le_count_iff_mem.2 <| mem_dedup.2 h]

Premises used: Iff.mpr, Multiset.mem_dedup, Multiset.one_le_count_iff_mem
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) (a ::ₘ s.erase a))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) (a ::ₘ s.erase a))

Tactic:
have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by
          simp
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) (a ::ₘ s.erase a))
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s)

Tactic:
rw [cons_erase h] at this

Premises used: Multiset.cons_erase
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s)
⊢ count a s ≤ HMul.hMul (α := ℕ) (fold max 0 (map (fun (a : α) ↦ count a s) s)) 1

Tactic:
simpa [mul_succ] using this

Premises used: Nat.mul_succ
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup

Tactic:
simp [count_eq_zero.2 h, Nat.zero_le]

Premises used: Iff.mpr, Nat.zero_le, Multiset.count_eq_zero
-- Module: Mathlib.Algebra.Order.Group.Nat
Goal:
⊢ OrderedSub ℕ

Tactic:
⟨fun m n k ↦ ?_⟩

Premises used: OrderedSub.mk
-- Module: Mathlib.Algebra.Order.Group.Nat
Goal:
refine : ∀ (m n k : ℕ), m - n ≤ k ↔ m ≤ k + n
⊢ OrderedSub ℕ

Tactic:
refine ⟨fun m n k ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Group.Nat
Goal:
m k : ℕ
⊢ m - 0 ≤ k ↔ m ≤ k + 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Nat
Goal:
m n : ℕ
ih : ∀ (k : ℕ), m - n ≤ k ↔ m ≤ k + n
k : ℕ
⊢ m - (n + 1) ≤ k ↔ m ≤ k + (n + 1)

Tactic:
simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]

Premises used: Nat.pred_le_iff, Nat.sub_succ, Nat.add_succ, Nat.succ_add
-- Module: Mathlib.Algebra.Order.Group.Nat
Goal:
m n k : ℕ
zero : ∀ (k : ℕ), m - 0 ≤ k ↔ m ≤ k + 0
succ : ∀ (n : ℕ) (ih : ∀ (k : ℕ), m - n ≤ k ↔ m ≤ k + n) (k : ℕ), m - (n + 1) ≤ k ↔ m ≤ k + (n + 1)
⊢ m - n ≤ k ↔ m ≤ k + n

Tactic:
induction n generalizing k with
  | zero => simp
  | succ n ih => simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]

Premises used: Nat.pred_le_iff, Nat.sub_succ, Nat.add_succ, Nat.zero, Nat.succ_add, Nat.succ
-- Module: Mathlib.Algebra.Order.Group.Nat
Goal:
n : ℕ
hn : n ≠ 0
⊢ StrictMono (β := ℕ) fun (x : ℕ) ↦ x ^ n

Tactic:
fun _ _ h ↦ Nat.pow_lt_pow_left h hn

Premises used: StrictMono, Nat.pow_lt_pow_left
-- Module: Mathlib.Algebra.Order.Group.Nat
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : Preorder α
hn : n ≠ 0
hf : StrictMono f
⊢ StrictMono (β := ℕ) fun (x : α) ↦ f x ^ n

Tactic:
(Nat.pow_left_strictMono hn).comp hf

Premises used: Nat.pow_left_strictMono, StrictMono.comp
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : Preorder α
a b : αᵐᵒᵖ
⊢ unop a ≤ unop b ↔ a ≤ b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ op a ≤ op b ↔ a ≤ b

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : αᵐᵒᵖ
hab : a ≤ b
c : αᵐᵒᵖ
⊢ unop a ≤ unop b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : αᵐᵒᵖ
⊢ unop a ≤ 1 ↔ a ≤ 1

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : αᵐᵒᵖ
⊢ 1 ≤ unop a ↔ 1 ≤ a

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : α
⊢ op a ≤ 1 ↔ a ≤ 1

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : α
⊢ 1 ≤ op a ↔ 1 ≤ a

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b : αᵐᵒᵖ
hab : a ≤ b
c : αᵐᵒᵖ
⊢ unop a ≤ unop b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
a : αᵐᵒᵖ
⊢ unop a ≤ 0 ↔ a ≤ 0

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
a : αᵐᵒᵖ
⊢ 0 ≤ unop a ↔ 0 ≤ a

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
a : α
⊢ op a ≤ 0 ↔ a ≤ 0

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
a : α
⊢ 0 ≤ op a ↔ 0 ≤ a

Tactic:
.rfl

Premises used: Iff.rfl, MulOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : αᵃᵒᵖ
hab : a ≤ b
c : αᵃᵒᵖ
⊢ unop a ≤ unop b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : αᵃᵒᵖ
⊢ unop a ≤ 1 ↔ a ≤ 1

Tactic:
.rfl

Premises used: Iff.rfl, AddOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : αᵃᵒᵖ
⊢ 1 ≤ unop a ↔ 1 ≤ a

Tactic:
.rfl

Premises used: Iff.rfl, AddOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : α
⊢ op a ≤ 1 ↔ a ≤ 1

Tactic:
.rfl

Premises used: Iff.rfl, AddOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
a : α
⊢ 1 ≤ op a ↔ 1 ≤ a

Tactic:
.rfl

Premises used: Iff.rfl, AddOpposite.unop
-- Module: Mathlib.Algebra.Order.Group.OrderIso
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
(OrderIso.inv α).symm_apply_le

Premises used: OrderIso.inv, OrderIso.symm_apply_le
-- Module: Mathlib.Algebra.Order.Group.OrderIso
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
(OrderIso.inv α).le_symm_apply

Premises used: OrderIso.inv, OrderIso.le_symm_apply
-- Module: Mathlib.Algebra.Order.Group.OrderIso
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a : α
h : ∀ (x : α), Eq (α := α) ((symm (mulRight a) : (a : α) → α) x : α) ((mulRight a⁻¹ : (a : α) → α) x : α)
⊢ Eq (α := α ≃o α) (symm (mulRight a)) (mulRight a⁻¹)

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Group.OrderIso
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a x : α
⊢ Eq (α := α) ((symm (mulRight a) : (a : α) → α) x : α) ((mulRight a⁻¹ : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Group.OrderIso
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
h : ∀ (x : α), Eq (α := α) ((symm (mulLeft a) : (a : α) → α) x : α) ((mulLeft a⁻¹ : (a : α) → α) x : α)
⊢ Eq (α := α ≃o α) (symm (mulLeft a)) (mulLeft a⁻¹)

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Group.OrderIso
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a x : α
⊢ Eq (α := α) ((symm (mulLeft a) : (a : α) → α) x : α) ((mulLeft a⁻¹ : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Group.PartialSups
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeSup α
inst_1 : Group α
inst_2 : Preorder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : MulLeftMono α
f : ι → α
c : α
i : ι
⊢ (partialSups fun (x : ι) ↦ c * f x : (a : ι) → α) i = HMul.hMul (β := α) c ((partialSups f : (a : ι) → α) i : α)

Tactic:
map_partialSups (OrderIso.mulLeft _) ..

Premises used: OrderIso.mulLeft, map_partialSups
-- Module: Mathlib.Algebra.Order.Group.PartialSups
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeSup α
inst_1 : Group α
inst_2 : Preorder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : MulRightMono α
f : ι → α
c : α
i : ι
⊢ (partialSups fun (x : ι) ↦ f x * c : (a : ι) → α) i = HMul.hMul (α := α) ((partialSups f : (a : ι) → α) i : α) c

Tactic:
map_partialSups (OrderIso.mulRight _) ..

Premises used: map_partialSups, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
a b : M
ha : a ∈ upperBounds s
hb : b ∈ upperBounds t
⊢ a * b ∈ upperBounds (s * t)

Tactic:
forall_mem_image2.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy)

Premises used: Iff.mpr, Set.forall_mem_image2, Set.Mem, setOf, upperBounds, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
⊢ upperBounds s * upperBounds t ⊆ upperBounds (s * t)

Tactic:
image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy

Premises used: Iff.mpr, Set.image2_subset_iff, mul_mem_upperBounds_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
a b : M
ha : a ∈ lowerBounds s
hb : b ∈ lowerBounds t
⊢ a * b ∈ lowerBounds (s * t)

Tactic:
mul_mem_upperBounds_mul (M := Mᵒᵈ) ha hb

Premises used: lowerBounds, Set.Mem, setOf, mul_mem_upperBounds_mul, OrderDual