awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ico a b)))
classical₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val))
⊢ map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have classical₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
Tactic: classical rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
Tactic: rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
Tactic: rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw₂ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioc a b)))
Tactic: rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioc a b)))
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw₃ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
  (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val))
Tactic: rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioc a b)))
rw₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val))
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
Tactic: rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have classical : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
Tactic: classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
Tactic: classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have classical₂ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioc a b)))
Tactic: classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioc a b)))
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have classical₃ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
  (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val))
Tactic: classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioc a b)))
classical₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val))
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have classical₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
Tactic: classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
Tactic: rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
Tactic: rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw₂ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioo a b)))
Tactic: rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioo a b)))
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw₃ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
  (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val))
Tactic: rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioo a b)))
rw₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val))
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
Tactic: rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have classical : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
Tactic: classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
Tactic: classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have classical₂ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioo a b)))
Tactic: classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioo a b)))
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have classical₃ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
  (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val))
Tactic: classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = Ioo (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioo a b)))
classical₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val))
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have classical₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
Tactic: classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ x + c) (Icc a b) = Icc (a + c) (b + c)
have simp_rw : map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
Tactic: simp_rw [add_comm _ c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ x + c) (Ico a b) = Ico (a + c) (b + c)
have simp_rw : map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
Tactic: simp_rw [add_comm _ c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)
have simp_rw : map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
Tactic: simp_rw [add_comm _ c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ map (fun (x : α) ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)
have simp_rw : map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
Tactic: simp_rw [add_comm _ c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
⊢ Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)
have inl : ∀ (h' : x < y), Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)
Tactic: rcases lt_or_ge x y with h' | h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
inl : ∀ (h' : x < y), Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)
have inr : ∀ (h' : y ≤ x), Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)
Tactic: rcases lt_or_ge x y with h' | h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)
have property : x ∈ Ico x (x + dx) \ Ico y (y + dy)
Tactic: use x
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)
have property : max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)
Tactic: use max x (x + dy)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ Pairwise fun (x y : ℤ) ↦ Disjoint (Ioc (a * b ^ x) (a * b ^ (x + 1))) (Ioc (a * b ^ y) (a * b ^ (y + 1)))
have simp_rw : Pairwise fun (x y : ℤ) ↦ Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
Tactic: simp_rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ Membership.mem (γ := Set α) ∅ x
have apply : m = n
Tactic: apply hmn
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b
have this : a * b ^ m < a * b ^ (m + 1)
Tactic: have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
have rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
⊢ 1 < b
have rwa₁ : ∀ (this : b ^ m * 1 < b ^ (m + 1)), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
rwa₁ : ∀ (this : b ^ m * 1 < b ^ (m + 1)), 1 < b
⊢ 1 < b
have rwa₂ : ∀ (this : b ^ m * 1 < b ^ m * b), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
rwa₁ : ∀ (this : b ^ m * 1 < b ^ (m + 1)), 1 < b
rwa₂ : ∀ (this : b ^ m * 1 < b ^ m * b), 1 < b
⊢ 1 < b
have rwa₃ : ∀ (this : 1 < b), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n
have hb : 1 < b
Tactic: have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n
have i1 : a * b ^ m < a * b ^ (n + 1)
Tactic: have i1 := hx.1.1.trans_le hx.2.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n
have i2 : a * b ^ n < a * b ^ (m + 1)
Tactic: have i2 := hx.2.1.trans_le hx.1.2