awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
⊢ countP p (n • s) = n * countP p s
have zero : countP p (HSMul.hSMul (α := ℕ) 0 s) = 0 * countP p s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
zero : countP p (HSMul.hSMul (α := ℕ) 0 s) = 0 * countP p s
⊢ countP p (n • s) = n * countP p s
have succ : ∀ (n : ℕ), countP p (n • s) = n * countP p s → countP p ((n + 1) • s) = (n + 1) * countP p s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
⊢ (n • s).dedup = s.dedup
have a : ∀ (a : α), count a (n • s).dedup = count a s.dedup
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
⊢ count a (n • s).dedup = count a s.dedup
have pos : ∀ (h : a ∈ s), count a (n • s).dedup = count a s.dedup
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
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
⊢ count a (n • s).dedup = count a s.dedup
have neg : ∀ (h : ¬a ∈ s), count a (n • s).dedup = count a s.dedup
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
s : Multiset α
⊢ count a (n • s) = n * count a s
have zero : count a (HSMul.hSMul (α := ℕ) 0 s) = 0 * count a s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
s : Multiset α
zero : count a (HSMul.hSMul (α := ℕ) 0 s) = 0 * count a s
⊢ count a (n • s) = n * count a s
have succ : ∀ (n : ℕ), count a (n • s) = n * count a s → count a ((n + 1) • s) = (n + 1) * count a s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
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} : β)
⊢ f = g
have h₁ : ∀ (s : Multiset α), Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) s : β) ((g : (a : Multiset α) → β) s : β)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
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 α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) s : β) ((g : (a : Multiset α) → β) s : β)
have h₁ : Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) 0 : β) ((g : (a : Multiset α) → β) 0 : β)
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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
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 : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : Multiset α) → β) s : β) ((g : (a : Multiset α) → β) s : β)
have 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) : β)
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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ count a (HSMul.hSMul (α := ℕ) (fold max 0 (map (fun (a : α) ↦ count a s) s)) s.dedup)
have rw : count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
Tactic: rw [count_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
have pos : ∀ (h : a ∈ s), count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
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
⊢ count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
have neg : ∀ (h : ¬a ∈ s), count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s) * count a s.dedup
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
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
have pos : count a s ≤ HMul.hMul (α := ℕ) (fold max 0 (map (fun (a : α) ↦ count a s) s)) 1
Tactic: grw [← one_le_count_iff_mem.2 <| mem_dedup.2 h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ HMul.hMul (α := ℕ) (fold max 0 (map (fun (a : α) ↦ count a s) s)) 1
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (hypothesis)
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 ≤ HMul.hMul (α := ℕ) (fold max 0 (map (fun (a : α) ↦ count a s) s)) 1
have this₁ : count a s ≤ fold max 0 (map (fun (a : α) ↦ count a s) s)
Tactic: rw [cons_erase h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Nat (goal)
Goal:
⊢ OrderedSub ℕ
have refine : ∀ (m n k : ℕ), m - n ≤ k ↔ m ≤ k + n
Tactic: refine ⟨fun m n k ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Nat (goal)
Goal:
m n k : ℕ
⊢ m - n ≤ k ↔ m ≤ k + n
have zero : ∀ (k : ℕ), m - 0 ≤ k ↔ m ≤ k + 0
Tactic: induction n generalizing k with
  | zero => simp
  | succ n ih => simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Nat (goal)
Goal:
m n k : ℕ
zero : ∀ (k : ℕ), m - 0 ≤ k ↔ m ≤ k + 0
⊢ m - n ≤ k ↔ m ≤ k + n
have succ : ∀ (n : ℕ) (ih : ∀ (k : ℕ), m - n ≤ k ↔ m ≤ k + n) (k : ℕ), m - (n + 1) ≤ k ↔ m ≤ k + (n + 1)
Tactic: induction n generalizing k with
  | zero => simp
  | succ n ih => simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.OrderIso (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a : α
⊢ Eq (α := α ≃o α) (symm (mulRight a)) (mulRight a⁻¹)
have h : ∀ (x : α), Eq (α := α) ((symm (mulRight a) : (a : α) → α) x : α) ((mulRight a⁻¹ : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.OrderIso (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
⊢ Eq (α := α ≃o α) (symm (mulLeft a)) (mulLeft a⁻¹)
have h : ∀ (x : α), Eq (α := α) ((symm (mulLeft a) : (a : α) → α) x : α) ((mulLeft a⁻¹ : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Bounds (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s / t) (a / b)
have rw : IsLUB (s * t⁻¹) (a * b⁻¹)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
⊢ sSup s⁻¹ = (sInf s)⁻¹
have rw : sSup ((fun (x : M) ↦ x⁻¹) '' s) = (sInf s)⁻¹
Tactic: rw [← image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf s⁻¹ = (sSup s)⁻¹
have rw : sInf ((fun (x : M) ↦ x⁻¹) '' s) = (sSup s)⁻¹
Tactic: rw [← image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sSup (s / t) = sSup s / sInf t
have rw : sSup (s * t⁻¹) = sSup s / sInf t
Tactic: rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
rw : sSup (s * t⁻¹) = sSup s / sInf t
⊢ sSup (s / t) = sSup s / sInf t
have rw₁ : sSup s * sSup t⁻¹ = sSup s / sInf t
Tactic: rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
rw : sSup (s * t⁻¹) = sSup s / sInf t
rw₁ : sSup s * sSup t⁻¹ = sSup s / sInf t
⊢ sSup (s / t) = sSup s / sInf t
have rw₂ : sSup s * (sInf t)⁻¹ = sSup s / sInf t
Tactic: rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
rw : sSup (s * t⁻¹) = sSup s / sInf t
rw₁ : sSup s * sSup t⁻¹ = sSup s / sInf t
rw₂ : sSup s * (sInf t)⁻¹ = sSup s / sInf t
⊢ sSup (s / t) = sSup s / sInf t
have rw₃ : sSup s * (sInf t)⁻¹ = sSup s * (sInf t)⁻¹
Tactic: rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf (s / t) = sInf s / sSup t
have rw : sInf (s * t⁻¹) = sInf s / sSup t
Tactic: rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
rw : sInf (s * t⁻¹) = sInf s / sSup t
⊢ sInf (s / t) = sInf s / sSup t
have rw₁ : sInf s * sInf t⁻¹ = sInf s / sSup t
Tactic: rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
rw : sInf (s * t⁻¹) = sInf s / sSup t
rw₁ : sInf s * sInf t⁻¹ = sInf s / sSup t
⊢ sInf (s / t) = sInf s / sSup t
have rw₂ : sInf s * (sSup t)⁻¹ = sInf s / sSup t
Tactic: rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
rw : sInf (s * t⁻¹) = sInf s / sSup t
rw₁ : sInf s * sInf t⁻¹ = sInf s / sSup t
rw₂ : sInf s * (sSup t)⁻¹ = sInf s / sSup t
⊢ sInf (s / t) = sInf s / sSup t
have rw₃ : sInf s * (sSup t)⁻¹ = sInf s * (sSup t)⁻¹
Tactic: rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
⊢ sSup s⁻¹ = (sInf s)⁻¹
have rw : ⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹
Tactic: rw [← image_inv_eq_inv, sSup_image]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
⊢ sInf s⁻¹ = (sSup s)⁻¹
have rw : ⨅ a ∈ s, a⁻¹ = (sSup s)⁻¹
Tactic: rw [← image_inv_eq_inv, sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
⊢ sSup (s / t) = sSup s / sInf t
have simp_rw : sSup (s * t⁻¹) = sSup s * (sInf t)⁻¹
Tactic: simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
simp_rw : sSup (s * t⁻¹) = sSup s * (sInf t)⁻¹
⊢ sSup (s / t) = sSup s / sInf t
have simp_rw₁ : sSup s * sSup t⁻¹ = sSup s * (sInf t)⁻¹
Tactic: simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
⊢ sInf (s / t) = sInf s / sSup t
have simp_rw : sInf (s * t⁻¹) = sInf s * (sSup t)⁻¹
Tactic: simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (goal)
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
simp_rw : sInf (s * t⁻¹) = sInf s * (sSup t)⁻¹
⊢ sInf (s / t) = sInf s / sSup t
have simp_rw₁ : sInf s * sInf t⁻¹ = sInf s * (sSup t)⁻¹
Tactic: simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)
have this : MulLeftMono α
Tactic: have := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)
have this₁ : MulRightMono α
Tactic: have := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)
have this : MulLeftMono α
Tactic: have := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)
have this₁ : MulRightMono α
Tactic: have := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)
have this : MulLeftMono α
Tactic: have := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)
have this₁ : MulRightMono α
Tactic: have := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)
have this : MulLeftMono α
Tactic: have := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)
have this₁ : MulRightMono α
Tactic: have := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
⊢ Iic a * Iio b ⊆ Iio (a * b)
have this : MulRightMono α
Tactic: have := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
⊢ Iio a * Iic b ⊆ Iio (a * b)
have this : MulLeftMono α
Tactic: have := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
⊢ Ioi a * Ici b ⊆ Ioi (a * b)
have this : MulLeftMono α
Tactic: have := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
⊢ Ici a * Ioi b ⊆ Ioi (a * b)
have this : MulRightMono α
Tactic: have := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c : α
⊢ a • Icc b c = Icc (a * b) (a * c)
have h : ∀ (x : α), x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)
have h : x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c x : α
h : x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)
⊢ x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)
have h₁ : x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ (fun (x : α) ↦ a • x) y ∈ Icc (a * b) (a * c)
have h : a * y ∈ Icc (a * b) (a * c)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ a * y ∈ Icc (a * b) (a * c)
have h : a * b ≤ a * y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
h : a * b ≤ a * y
⊢ a * y ∈ Icc (a * b) (a * c)
have h₁ : a * y ≤ a * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c x : α
habx : a * b ≤ x
hxac : x ≤ a * c
⊢ x ∈ a • Icc b c
have h : ∀ (y : α) (hy : 1 ≤ y) (habx : a * b ≤ a * b * y) (hxac : a * b * y ≤ a * c), a * b * y ∈ a • Icc b c
Tactic: obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le habx
Cleared hypotheses: x, habx, hxac
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ a * b * y ∈ a • Icc b c
have h : b * y ≤ c
Tactic: refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ b * y ≤ c
have h : ∀ (hxac : a * (b * y) ≤ a * c), b * y ≤ c
Tactic: rwa [mul_assoc, mul_le_mul_iff_left] at hxac
Cleared hypotheses: hxac
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
h : ∀ (hxac : a * (b * y) ≤ a * c), b * y ≤ c
⊢ b * y ≤ c
have h₁ : ∀ (hxac : b * y ≤ c), b * y ≤ c
Tactic: rwa [mul_assoc, mul_le_mul_iff_left] at hxac
Cleared hypotheses: hxac
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b * Icc c d = Icc (a * c) (b * d)
have refine : ∀ x ∈ Icc (a * c) (b * d), ∀ (hacx : a * c ≤ x) (hxbd : x ≤ b * d), x ∈ Icc a b * Icc c d
Tactic: refine (Icc_mul_Icc_subset' _ _ _ _).antisymm fun x ⟨hacx, hxbd⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
h : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
⊢ x ∈ Icc a b * Icc c d
have inl : ∀ (hxbc : x ≤ b * c), x ∈ Icc a b * Icc c d
Tactic: obtain hxbc | hbcx := le_total x (b * c)