awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Icc a b) = map (addRightEmbedding c) (Icc a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Icc a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Icc a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Icc a b))
    (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := ⋯ : α ↪ α } : (a : α) → α) (Icc a b))
⊢ image (fun (x : α) ↦ x + c) (Icc a b) = Icc (a + c) (b + c)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Icc a b)) (image (fun (h : α) ↦ h + c) (Icc a b))
Tactic: rw [← map_add_right_Icc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
⊢ image (fun (x : α) ↦ x + c) (Ico a b) = Ico (a + c) (b + c)
have rw : image (fun (x : α) ↦ x + c) (Ico a b) = map (addRightEmbedding c) (Ico a b)
Tactic: rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ico a b) = map (addRightEmbedding c) (Ico a b)
⊢ image (fun (x : α) ↦ x + c) (Ico a b) = Ico (a + c) (b + c)
have rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ico a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ico a b))
Tactic: rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ico a b) = map (addRightEmbedding c) (Ico a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ico a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ico a b))
⊢ image (fun (x : α) ↦ x + c) (Ico a b) = Ico (a + c) (b + c)
have rw₂ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ico a b))
  (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := sorry : α ↪ α } : (a : α) → α) (Ico a b))
Tactic: rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ico a b) = map (addRightEmbedding c) (Ico a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ico a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ico a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ico a b))
    (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ico a b))
⊢ image (fun (x : α) ↦ x + c) (Ico a b) = Ico (a + c) (b + c)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ico a b)) (image (fun (h : α) ↦ h + c) (Ico a b))
Tactic: rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
⊢ image (fun (x : α) ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)
have rw : image (fun (x : α) ↦ x + c) (Ioc a b) = map (addRightEmbedding c) (Ioc a b)
Tactic: rw [← map_add_right_Ioc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioc a b) = map (addRightEmbedding c) (Ioc a b)
⊢ image (fun (x : α) ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)
have rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioc a b))
Tactic: rw [← map_add_right_Ioc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioc a b) = map (addRightEmbedding c) (Ioc a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioc a b))
⊢ image (fun (x : α) ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)
have rw₂ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b))
  (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := sorry : α ↪ α } : (a : α) → α) (Ioc a b))
Tactic: rw [← map_add_right_Ioc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioc a b) = map (addRightEmbedding c) (Ioc a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioc a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b))
    (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ioc a b))
⊢ image (fun (x : α) ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b)) (image (fun (h : α) ↦ h + c) (Ioc a b))
Tactic: rw [← map_add_right_Ioc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
⊢ image (fun (x : α) ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)
have rw : image (fun (x : α) ↦ x + c) (Ioo a b) = map (addRightEmbedding c) (Ioo a b)
Tactic: rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioo a b) = map (addRightEmbedding c) (Ioo a b)
⊢ image (fun (x : α) ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)
have rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioo a b))
Tactic: rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioo a b) = map (addRightEmbedding c) (Ioo a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioo a b))
⊢ image (fun (x : α) ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)
have rw₂ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b))
  (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := sorry : α ↪ α } : (a : α) → α) (Ioo a b))
Tactic: rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioo a b) = map (addRightEmbedding c) (Ioo a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioo a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b))
    (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ioo a b))
⊢ image (fun (x : α) ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b)) (image (fun (h : α) ↦ h + c) (Ioo a b))
Tactic: rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]
-- 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) (Icc a b) = Icc (c + a) (c + b)
have rw : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = Icc (c + a) (c + b)
Tactic: rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
Tactic: rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw₂ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
Tactic: rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw₃ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
  (dedup (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val))
Tactic: rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
rw₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val))
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
Tactic: rw [Icc, Icc, ← Finset.image_add_left_Icc, 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) (Icc a b) = Icc (c + a) (c + b)
have classical : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = Icc (c + a) (c + b)
Tactic: classical rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have classical₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
Tactic: classical rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have classical₂ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
Tactic: classical rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have classical₃ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
  (dedup (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val))
Tactic: classical rw [Icc, Icc, ← Finset.image_add_left_Icc, 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.Icc a b).val = Icc (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
classical₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val))
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have classical₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
Tactic: classical rw [Icc, Icc, ← Finset.image_add_left_Icc, 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) (Ico a b) = Ico (c + a) (c + b)
have rw : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
Tactic: 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 : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + b)).val
Tactic: 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 : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + b)).val
⊢ map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have rw₂ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ico a b)))
Tactic: 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 : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ico a b)))
⊢ map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have rw₃ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
  (dedup (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val))
Tactic: 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 : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ico a b)))
rw₃ :
  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 rw₄ : Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
Tactic: 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) (Ico a b) = Ico (c + a) (c + b)
have classical : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
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 : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
⊢ map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + 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 : α
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
⊢ 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)
  (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ico a b)))
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 : α
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)))
⊢ 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)
  (dedup (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]