awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : s + t = 0
⊢ -s = t
have obtain : ∀ (a b : α) (hab : a + b = 0) (h : HAdd.hAdd (α := NonemptyInterval α) (pure a) (pure b) = 0),
  Eq (α := NonemptyInterval α) (-pure a) (pure b)
Tactic: obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
a b : α
hab : a + b = 0
h : HAdd.hAdd (α := NonemptyInterval α) (pure a) (pure b) = 0
⊢ Eq (α := NonemptyInterval α) (-pure a) (pure b)
have rw : Eq (α := NonemptyInterval α) (pure (-a)) (pure b)
Tactic: rw [neg_pure, neg_eq_of_add_eq_zero_right hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
a b : α
hab : a + b = 0
h : HAdd.hAdd (α := NonemptyInterval α) (pure a) (pure b) = 0
rw : Eq (α := NonemptyInterval α) (pure (-a)) (pure b)
⊢ Eq (α := NonemptyInterval α) (-pure a) (pure b)
have rw₁ : Eq (α := NonemptyInterval α) (pure b) (pure b)
Tactic: rw [neg_pure, neg_eq_of_add_eq_zero_right hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 s t : NonemptyInterval α
⊢ s / t = s * t⁻¹
have refine_1 : (s / t).toProd.1 = (s * t⁻¹).toProd.1
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 s t : NonemptyInterval α
refine_1 : (s / t).toProd.1 = (s * t⁻¹).toProd.1
⊢ s / t = s * t⁻¹
have refine_2 : (s / t).toProd.2 = (s * t⁻¹).toProd.2
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t s : NonemptyInterval α
⊢ s⁻¹⁻¹ = s
have toProd : s⁻¹⁻¹.toProd = s.toProd
Tactic: apply NonemptyInterval.ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 s t : NonemptyInterval α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹
have refine_1 : (s * t)⁻¹.toProd.1 = (t⁻¹ * s⁻¹).toProd.1
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 s t : NonemptyInterval α
refine_1 : (s * t)⁻¹.toProd.1 = (t⁻¹ * s⁻¹).toProd.1
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹
have refine_2 : (s * t)⁻¹.toProd.2 = (t⁻¹ * s⁻¹).toProd.2
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 s t : NonemptyInterval α
h : s * t = 1
⊢ s⁻¹ = t
have obtain : ∀ (a b : α) (hab : a * b = 1) (h : HMul.hMul (α := NonemptyInterval α) (pure a) (pure b) = 1),
  Eq (α := NonemptyInterval α) (pure a)⁻¹ (pure b)
Tactic: obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
a b : α
hab : a * b = 1
h : HMul.hMul (α := NonemptyInterval α) (pure a) (pure b) = 1
⊢ Eq (α := NonemptyInterval α) (pure a)⁻¹ (pure b)
have rw : Eq (α := NonemptyInterval α) (pure a⁻¹) (pure b)
Tactic: rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
a b : α
hab : a * b = 1
h : HMul.hMul (α := NonemptyInterval α) (pure a) (pure b) = 1
rw : Eq (α := NonemptyInterval α) (pure a⁻¹) (pure b)
⊢ Eq (α := NonemptyInterval α) (pure a)⁻¹ (pure b)
have rw₁ : Eq (α := NonemptyInterval α) (pure b) (pure b)
Tactic: rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have bot : ⊥ * t = 1 ↔ ∃ (a : α) (b : α), Eq (α := Interval α) ⊥ (pure a) ∧ t = pure b ∧ a * b = 1
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
bot : ⊥ * t = 1 ↔ ∃ (a : α) (b : α), Eq (α := Interval α) ⊥ (pure a) ∧ t = pure b ∧ a * b = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have coe : ∀ (a : NonemptyInterval α),
  (↑a : Interval α) * t = 1 ↔ ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ t = pure b ∧ a_1 * b = 1
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
t : Interval α
a : NonemptyInterval α
⊢ (↑a : Interval α) * t = 1 ↔ ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ t = pure b ∧ a_1 * b = 1
have coe : (↑a : Interval α) * ⊥ = 1 ↔
  ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ Eq (α := Interval α) ⊥ (pure b) ∧ a_1 * b = 1
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
t : Interval α
a : NonemptyInterval α
coe :
  (↑a : Interval α) * ⊥ = 1 ↔
    ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ Eq (α := Interval α) ⊥ (pure b) ∧ a_1 * b = 1
⊢ (↑a : Interval α) * t = 1 ↔ ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ t = pure b ∧ a_1 * b = 1
have coe₁ : ∀ (a_1 : NonemptyInterval α),
  (↑a : Interval α) * (↑a_1 : Interval α) = 1 ↔
    ∃ (a_2 : α) (b : α), (↑a : Interval α) = pure a_2 ∧ (↑a_1 : Interval α) = pure b ∧ a_2 * b = 1
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a a_1 : NonemptyInterval α
⊢ (↑a : Interval α) * (↑a_1 : Interval α) = 1 ↔
    ∃ (a_2 : α) (b : α), (↑a : Interval α) = pure a_2 ∧ (↑a_1 : Interval α) = pure b ∧ a_2 * b = 1
have coe : a * a_1 = 1 ↔ ∃ (a_2 : α) (b : α), a = NonemptyInterval.pure a_2 ∧ a_1 = NonemptyInterval.pure b ∧ a_2 * b = 1
Tactic: simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval,
      Interval.coe_inj, NonemptyInterval.coe_eq_pure]
-- 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 α
a b c : α
⊢ map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)
have rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (c + a) (c + b)
Tactic: rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
-- 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 α
a b c : α
⊢ map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)
have rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (a + c) (b + c)
Tactic: rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
-- 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 α
a b c : α
⊢ map (addLeftEmbedding c) (Ico a b) = Ico (c + a) (c + b)
have rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (c + a) (c + b)
Tactic: rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
-- 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 α
a b c : α
⊢ map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)
have rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (a + c) (b + c)
Tactic: rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
-- 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 α
a b c : α
⊢ map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)
have rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)
Tactic: rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
-- 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 α
a b c : α
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)
have rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
Tactic: rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
-- 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 α
a b c : α
⊢ map (addLeftEmbedding c) (Ioo a b) = Ioo (c + a) (c + b)
have rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)
Tactic: rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
-- 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 α
a b c : α
⊢ map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)
have rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)
Tactic: rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
-- 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 : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw : image (fun (x : α) ↦ c + x) (Icc a b) = map (addLeftEmbedding c) (Icc a b)
Tactic: rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Icc a b) = map (addLeftEmbedding c) (Icc a b)
⊢ image (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Icc a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Icc a b))
Tactic: rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Icc a b) = map (addLeftEmbedding c) (Icc a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Icc a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Icc a b))
⊢ image (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw₂ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Icc a b))
  (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := sorry : α ↪ α } : (a : α) → α) (Icc a b))
Tactic: rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Icc a b) = map (addLeftEmbedding c) (Icc a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Icc a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Icc a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Icc a b))
    (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := ⋯ : α ↪ α } : (a : α) → α) (Icc a b))
⊢ image (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Icc a b)) (image (fun (h : α) ↦ c + h) (Icc a b))
Tactic: rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have rw : image (fun (x : α) ↦ c + x) (Ico a b) = map (addLeftEmbedding c) (Ico a b)
Tactic: rw [← map_add_left_Ico, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ico a b) = map (addLeftEmbedding c) (Ico a b)
⊢ image (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ico a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ico a b))
Tactic: rw [← map_add_left_Ico, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ico a b) = map (addLeftEmbedding c) (Ico a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ico a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ico a b))
⊢ image (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have rw₂ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ico a b))
  (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := sorry : α ↪ α } : (a : α) → α) (Ico a b))
Tactic: rw [← map_add_left_Ico, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ico a b) = map (addLeftEmbedding c) (Ico a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ico a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ico a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ico a b))
    (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ico a b))
⊢ image (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ico a b)) (image (fun (h : α) ↦ c + h) (Ico a b))
Tactic: rw [← map_add_left_Ico, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw : image (fun (x : α) ↦ c + x) (Ioc a b) = map (addLeftEmbedding c) (Ioc a b)
Tactic: rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioc a b) = map (addLeftEmbedding c) (Ioc a b)
⊢ image (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioc a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ioc a b))
Tactic: rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioc a b) = map (addLeftEmbedding c) (Ioc a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioc a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ioc a b))
⊢ image (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw₂ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioc a b))
  (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := sorry : α ↪ α } : (a : α) → α) (Ioc a b))
Tactic: rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioc a b) = map (addLeftEmbedding c) (Ioc a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioc a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ioc a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioc a b))
    (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ioc a b))
⊢ image (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioc a b)) (image (fun (h : α) ↦ c + h) (Ioc a b))
Tactic: rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw : image (fun (x : α) ↦ c + x) (Ioo a b) = map (addLeftEmbedding c) (Ioo a b)
Tactic: rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioo a b) = map (addLeftEmbedding c) (Ioo a b)
⊢ image (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioo a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ioo a b))
Tactic: rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioo a b) = map (addLeftEmbedding c) (Ioo a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioo a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ioo a b))
⊢ image (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw₂ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioo a b))
  (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := sorry : α ↪ α } : (a : α) → α) (Ioo a b))
Tactic: rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, 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 : α) ↦ c + x) (Ioo a b) = map (addLeftEmbedding c) (Ioo a b)
rw₁ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioo a b)) (image (⇑(addLeftEmbedding c) : (a : α) → α) (Ioo a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioo a b))
    (image (⇑{ toFun := fun (h : α) ↦ c + h, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ioo a b))
⊢ image (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
have rw₃ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioo a b)) (image (fun (h : α) ↦ c + h) (Ioo a b))
Tactic: rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, 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) (Icc a b) = Icc (a + c) (b + c)
have rw : image (fun (x : α) ↦ x + c) (Icc a b) = map (addRightEmbedding 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 : α
rw : image (fun (x : α) ↦ x + c) (Icc a b) = map (addRightEmbedding c) (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 (⇑(addRightEmbedding c) : (a : α) → α) (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 : α
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))
⊢ 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 (⇑{ toFun := fun (h : α) ↦ h + c, inj' := sorry : α ↪ α } : (a : α) → α) (Icc a b))
Tactic: rw [← map_add_right_Icc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]