awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

Premises used: WithBot.some, congr_arg, mul_inv_rev
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
h : HMul.hMul (α := Interval α) none none = 1
⊢ Eq.{u_2 + 1} (α := Interval α) none⁻¹ none

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
h : HMul.hMul (α := Interval α) none none = 1
⊢ Eq.{u_2 + 1} (α := Interval α) none⁻¹ none

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h)
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t_1 : Interval α
t : NonemptyInterval α
h : none * some t = 1
⊢ none⁻¹ = some t

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t_1 : Interval α
t : NonemptyInterval α
h : none * some t = 1
⊢ none⁻¹ = some t

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h)
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
h : some s * none = 1
⊢ (some s)⁻¹ = none

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
h : some s * none = 1
⊢ (some s)⁻¹ = none

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h)
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : some s * some t = 1
⊢ (some s)⁻¹ = some t

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : some s * some t = 1
⊢ (some s)⁻¹ = some t

Tactic:
congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h)

Premises used: WithBot.some, WithBot.coe_injective, Interval, congr_arg, inv_eq_of_mul_eq_one_right, WithBot.map
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : some s * some t = 1
⊢ (some s)⁻¹ = some t

Tactic:
exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h)

Premises used: WithBot.some, WithBot.coe_injective, congr_arg, inv_eq_of_mul_eq_one_right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : some s * some t = 1
⊢ (some s)⁻¹ = some t

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h)

Premises used: WithBot.some, WithBot.coe_injective, congr_arg, inv_eq_of_mul_eq_one_right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ 0 ≤ s.length

Tactic:
sub_nonneg_of_le s.fst_le_snd

Premises used: sub_nonneg_of_le, NonemptyInterval.length, NonemptyInterval.fst_le_snd
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
a : α
⊢ length (pure a) = 0

Tactic:
sub_self _

Premises used: sub_self, NonemptyInterval.length
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
⊢ Eq.{u_2 + 1} (α := α) (length 0) 0

Tactic:
length_pure _

Premises used: NonemptyInterval.length_pure
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ (-s).length = s.length

Tactic:
neg_sub_neg _ _

Premises used: NonemptyInterval.length, neg_sub_neg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s + t).length = s.length + t.length

Tactic:
add_sub_add_comm _ _ _ _

Premises used: NonemptyInterval.length, add_sub_add_comm
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s - t).length = s.length + t.length

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
f : ι → NonemptyInterval α
s : Finset ι
⊢ Eq.{u_2 + 1} (α := α) (length (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).length)

Tactic:
map_sum (⟨⟨length, length_zero⟩, length_add⟩ : NonemptyInterval α →+ α) _ _

Premises used: NonemptyInterval.length_zero, AddMonoidHom.mk, map_sum, ZeroHom.mk, NonemptyInterval.length_add, NonemptyInterval.length
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
a : α
⊢ length (pure a) = 0

Tactic:
NonemptyInterval.length_pure _

Premises used: Interval.length, NonemptyInterval.length_pure
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
⊢ Eq.{u_2 + 1} (α := α) (length 0) 0

Tactic:
length_pure _

Premises used: Interval.pure, Interval.length_pure
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
⊢ Eq.{u_2 + 1} (α := α) (length ⊥) 0

Tactic:
rfl

Premises used: Interval.length, rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
x : Interval α
⊢ (⊥ + x).length ≤ length ⊥ + x.length

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
x : Interval α
⊢ (x + ⊥).length ≤ x.length + length ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
s t : Interval α
⊢ (s - t).length ≤ s.length + t.length

Tactic:
simpa [sub_eq_add_neg] using length_add_le s (-t)

Premises used: sub_eq_add_neg, Interval.length_add_le, Neg.neg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
f : ι → Interval α
s : Finset ι
⊢ LE.le.{u_2} (α := α) (length (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).length)

Tactic:
Finset.le_sum_of_subadditive _ length_zero.le length_add_le _ _

Premises used: Finset.le_sum_of_subadditive
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (c + a) (c + b)
⊢ map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]

Premises used: Finset.coe_Icc, Finset.coe_inj, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (c + a) (c + b)

Tactic:
Set.image_const_add_Icc _ _ _

Premises used: Set.image_const_add_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (c + a) (c + b)

Tactic:
exact Set.image_const_add_Icc _ _ _

Premises used: Set.image_const_add_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (a + c) (b + c)
⊢ map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]

Premises used: Finset.coe_Icc, Finset.coe_inj, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (a + c) (b + c)

Tactic:
Set.image_add_const_Icc _ _ _

Premises used: Set.image_add_const_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Icc a b = Set.Icc (a + c) (b + c)

Tactic:
exact Set.image_add_const_Icc _ _ _

Premises used: Set.image_add_const_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (c + a) (c + b)
⊢ map (addLeftEmbedding c) (Ico a b) = Ico (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]

Premises used: Finset.coe_Ico, Finset.coe_inj, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (c + a) (c + b)

Tactic:
Set.image_const_add_Ico _ _ _

Premises used: Set.image_const_add_Ico
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (c + a) (c + b)

Tactic:
exact Set.image_const_add_Ico _ _ _

Premises used: Set.image_const_add_Ico
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (a + c) (b + c)
⊢ map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]

Premises used: Finset.coe_Ico, Finset.coe_inj, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (a + c) (b + c)

Tactic:
Set.image_add_const_Ico _ _ _

Premises used: Set.image_add_const_Ico
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ico a b = Set.Ico (a + c) (b + c)

Tactic:
exact Set.image_add_const_Ico _ _ _

Premises used: Set.image_add_const_Ico
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)
⊢ map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]

Premises used: Finset.coe_inj, Finset.coe_Ioc, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)

Tactic:
Set.image_const_add_Ioc _ _ _

Premises used: Set.image_const_add_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)

Tactic:
exact Set.image_const_add_Ioc _ _ _

Premises used: Set.image_const_add_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]

Premises used: Finset.coe_inj, Finset.coe_Ioc, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)

Tactic:
Set.image_add_const_Ioc _ _ _

Premises used: Set.image_add_const_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)

Tactic:
exact Set.image_add_const_Ioc _ _ _

Premises used: Set.image_add_const_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)
⊢ map (addLeftEmbedding c) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]

Premises used: Finset.coe_inj, Finset.coe_Ioo, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)

Tactic:
Set.image_const_add_Ioo _ _ _

Premises used: Set.image_const_add_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addLeftEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)

Tactic:
exact Set.image_const_add_Ioo _ _ _

Premises used: Set.image_const_add_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)
⊢ map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]

Premises used: Finset.coe_inj, Finset.coe_Ioo, Finset.coe_map
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)

Tactic:
Set.image_add_const_Ioo _ _ _

Premises used: Set.image_add_const_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
⊢ (⇑(addRightEmbedding c) : (a : α) → α) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)

Tactic:
exact Set.image_add_const_Ioo _ _ _

Premises used: Set.image_add_const_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
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))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Icc a b)) (image (fun (h : α) ↦ c + h) (Icc a b))
⊢ image (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Premises used: addLeftEmbedding, Finset.map_eq_image, Finset.map_add_left_Icc, Function.Embedding.coeFn_mk
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
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))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ico a b)) (image (fun (h : α) ↦ c + h) (Ico a b))
⊢ image (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
rw [← map_add_left_Ico, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Premises used: addLeftEmbedding, Finset.map_add_left_Ico, Finset.map_eq_image, Function.Embedding.coeFn_mk
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
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))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioc a b)) (image (fun (h : α) ↦ c + h) (Ioc a b))
⊢ image (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Premises used: addLeftEmbedding, Finset.map_eq_image, Finset.map_add_left_Ioc, Function.Embedding.coeFn_mk
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
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))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ c + x) (Ioo a b)) (image (fun (h : α) ↦ c + h) (Ioo a b))
⊢ image (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Premises used: addLeftEmbedding, Finset.map_add_left_Ioo, Finset.map_eq_image, Function.Embedding.coeFn_mk
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
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))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Icc a b)) (image (fun (h : α) ↦ h + c) (Icc a b))
⊢ image (fun (x : α) ↦ x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
rw [← map_add_right_Icc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Premises used: Finset.map_eq_image, Function.Embedding.coeFn_mk, Finset.map_add_right_Icc, addRightEmbedding
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
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))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ico a b)) (image (fun (h : α) ↦ h + c) (Ico a b))
⊢ image (fun (x : α) ↦ x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Premises used: Finset.map_add_right_Ico, Finset.map_eq_image, Function.Embedding.coeFn_mk, addRightEmbedding