awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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))
classical₄ classical₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = 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]

Premises used: Multiset.Ioc, Finset.image_val, Finset.image_add_left_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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))
rw₄ rw₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = 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]

Premises used: Multiset.Nodup.map, Finset.image_add_left_Ioo, add_right_injective, Finset.nodup, Multiset.Ioo, Multiset.Nodup.dedup, Finset.image_val
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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))
classical₄ classical₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioo a b).val)
⊢ map (fun (x : α) ↦ c + x) (Ioo a b) = 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]

Premises used: Finset.image_add_left_Ioo, Multiset.Ioo, Finset.image_val
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
simp_rw : map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
⊢ map (fun (x : α) ↦ x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
map_add_left_Icc _ _ _

Premises used: Multiset.map_add_left_Icc
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
exact map_add_left_Icc _ _ _

Premises used: Multiset.map_add_left_Icc
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
simp_rw : map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
⊢ map (fun (x : α) ↦ x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
map_add_left_Ico _ _ _

Premises used: Multiset.map_add_left_Ico
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
exact map_add_left_Ico _ _ _

Premises used: Multiset.map_add_left_Ico
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
simp_rw : map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
⊢ map (fun (x : α) ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
map_add_left_Ioc _ _ _

Premises used: Multiset.map_add_left_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
exact map_add_left_Ioc _ _ _

Premises used: Multiset.map_add_left_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
simp_rw : map (fun (x : α) ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
⊢ map (fun (x : α) ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
map_add_left_Ioo _ _ _

Premises used: Multiset.map_add_left_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Multiset
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)

Tactic:
exact map_add_left_Ioo _ _ _

Premises used: Multiset.map_add_left_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a c d : α
⊢ a⁻¹ ∈ Icc c d ↔ a ∈ Icc d⁻¹ c⁻¹

Tactic:
and_comm.trans <| and_congr inv_le' le_inv'

Premises used: inv_le', Set.Mem, setOf, and_comm, Set.Icc, Iff.trans, le_inv', and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a c d : α
⊢ a⁻¹ ∈ Ico c d ↔ a ∈ Ioc d⁻¹ c⁻¹

Tactic:
and_comm.trans <| and_congr inv_lt' le_inv'

Premises used: inv_lt', Set.Mem, setOf, and_comm, Set.Ico, Iff.trans, le_inv', and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a c d : α
⊢ a⁻¹ ∈ Ioc c d ↔ a ∈ Ico d⁻¹ c⁻¹

Tactic:
and_comm.trans <| and_congr inv_le' lt_inv'

Premises used: inv_le', Set.Ioc, Set.Mem, setOf, and_comm, lt_inv', Iff.trans, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a c d : α
⊢ a⁻¹ ∈ Ioo c d ↔ a ∈ Ioo d⁻¹ c⁻¹

Tactic:
and_comm.trans <| and_congr inv_lt' lt_inv'

Premises used: inv_lt', Set.Mem, setOf, and_comm, lt_inv', Iff.trans, Set.Ioo, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Icc c d ↔ a ∈ Icc (c - b) (d - b)

Tactic:
(and_congr sub_le_iff_le_add le_sub_iff_add_le).symm

Premises used: Set.Mem, setOf, sub_le_iff_le_add, Set.Icc, le_sub_iff_add_le, Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Ico c d ↔ a ∈ Ico (c - b) (d - b)

Tactic:
(and_congr sub_le_iff_le_add lt_sub_iff_add_lt).symm

Premises used: Set.Mem, setOf, sub_le_iff_le_add, Set.Ico, lt_sub_iff_add_lt, Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Ioc c d ↔ a ∈ Ioc (c - b) (d - b)

Tactic:
(and_congr sub_lt_iff_lt_add le_sub_iff_add_le).symm

Premises used: Set.Ioc, Set.Mem, setOf, sub_lt_iff_lt_add, le_sub_iff_add_le, Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Ioo c d ↔ a ∈ Ioo (c - b) (d - b)

Tactic:
(and_congr sub_lt_iff_lt_add lt_sub_iff_add_lt).symm

Premises used: Set.Mem, setOf, sub_lt_iff_lt_add, lt_sub_iff_add_lt, Set.Ioo, Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Icc c d ↔ b ∈ Icc (c - a) (d - a)

Tactic:
(and_congr sub_le_iff_le_add' le_sub_iff_add_le').symm

Premises used: Set.Mem, setOf, le_sub_iff_add_le', Set.Icc, sub_le_iff_le_add', Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Ico c d ↔ b ∈ Ico (c - a) (d - a)

Tactic:
(and_congr sub_le_iff_le_add' lt_sub_iff_add_lt').symm

Premises used: lt_sub_iff_add_lt', Set.Mem, setOf, Set.Ico, sub_le_iff_le_add', Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Ioc c d ↔ b ∈ Ioc (c - a) (d - a)

Tactic:
(and_congr sub_lt_iff_lt_add' le_sub_iff_add_le').symm

Premises used: Set.Ioc, Set.Mem, setOf, le_sub_iff_add_le', sub_lt_iff_lt_add', Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a + b ∈ Ioo c d ↔ b ∈ Ioo (c - a) (d - a)

Tactic:
(and_congr sub_lt_iff_lt_add' lt_sub_iff_add_lt').symm

Premises used: lt_sub_iff_add_lt', Set.Mem, setOf, sub_lt_iff_lt_add', Set.Ioo, Iff.symm, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Icc c d ↔ a ∈ Icc (c + b) (d + b)

Tactic:
and_congr le_sub_iff_add_le sub_le_iff_le_add

Premises used: Set.Mem, setOf, sub_le_iff_le_add, Set.Icc, le_sub_iff_add_le, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Ico c d ↔ a ∈ Ico (c + b) (d + b)

Tactic:
and_congr le_sub_iff_add_le sub_lt_iff_lt_add

Premises used: Set.Mem, setOf, Set.Ico, sub_lt_iff_lt_add, le_sub_iff_add_le, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Ioc c d ↔ a ∈ Ioc (c + b) (d + b)

Tactic:
and_congr lt_sub_iff_add_lt sub_le_iff_le_add

Premises used: Set.Ioc, Set.Mem, setOf, sub_le_iff_le_add, lt_sub_iff_add_lt, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Ioo c d ↔ a ∈ Ioo (c + b) (d + b)

Tactic:
and_congr lt_sub_iff_add_lt sub_lt_iff_lt_add

Premises used: Set.Mem, setOf, sub_lt_iff_lt_add, lt_sub_iff_add_lt, Set.Ioo, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Icc c d ↔ b ∈ Icc (a - d) (a - c)

Tactic:
and_comm.trans <| and_congr sub_le_comm le_sub_comm

Premises used: Set.Mem, setOf, and_comm, sub_le_comm, Set.Icc, Iff.trans, and_congr, le_sub_comm
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Ico c d ↔ b ∈ Ioc (a - d) (a - c)

Tactic:
and_comm.trans <| and_congr sub_lt_comm le_sub_comm

Premises used: sub_lt_comm, Set.Mem, setOf, and_comm, Set.Ico, Iff.trans, and_congr, le_sub_comm
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Ioc c d ↔ b ∈ Ico (a - d) (a - c)

Tactic:
and_comm.trans <| and_congr sub_le_comm lt_sub_comm

Premises used: Set.Ioc, Set.Mem, setOf, and_comm, lt_sub_comm, sub_le_comm, Iff.trans, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ a - b ∈ Ioo c d ↔ b ∈ Ioo (a - d) (a - c)

Tactic:
and_comm.trans <| and_congr sub_lt_comm lt_sub_comm

Premises used: sub_lt_comm, Set.Mem, setOf, and_comm, lt_sub_comm, Iff.trans, Set.Ioo, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
R : Type u_2
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
x y z : R
⊢ |x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z)

Tactic:
abs_le.trans <| and_comm.trans <| and_congr sub_le_comm neg_le_sub_iff_le_add

Premises used: abs_le, and_comm, sub_le_comm, Iff.trans, neg_le_sub_iff_le_add, and_congr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b

Tactic:
simp only [sub_mem_Icc_iff_right, sub_self, sub_zero]

Premises used: sub_self, sub_zero, Set.sub_mem_Icc_iff_right
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

Tactic:
simp only [sub_mem_Ico_iff_right, sub_self, sub_zero]

Premises used: sub_self, sub_zero, Set.sub_mem_Ico_iff_right
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

Tactic:
simp only [sub_mem_Ioc_iff_right, sub_self, sub_zero]

Premises used: sub_self, sub_zero, Set.sub_mem_Ioc_iff_right
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ioo 0 b ↔ a ∈ Ioo 0 b

Tactic:
simp only [sub_mem_Ioo_iff_right, sub_self, sub_zero]

Premises used: sub_self, sub_zero, Set.sub_mem_Ioo_iff_right
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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)
inr : ∀ (h' : y ≤ x), 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)

Tactic:
rcases lt_or_ge x y with h' | h'

Premises used: lt_or_ge
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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
property : x ∈ Ico x (x + dx) \ Ico y (y + dy)
⊢ Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)

Tactic:
use x
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)

Tactic:
simp [*, not_le.2 h']

Premises used: not_le, Iff.mpr
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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
property : max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)
⊢ Nonempty.{u_1 + 1} (↑(Ico x (x + dx) \ Ico y (y + dy)) : Type u_1)

Tactic:
use max x (x + dy)

Premises used: HAdd.hAdd, Max.max
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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
⊢ max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
simp_rw : Pairwise fun (x y : ℤ) ↦ Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
⊢ Pairwise fun (x y : ℤ) ↦ Disjoint (Ioc (a * b ^ x) (a * b ^ (x + 1))) (Ioc (a * b ^ y) (a * b ^ (y + 1)))

Tactic:
simp_rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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))
apply : m = n
⊢ Membership.mem (γ := Set α) ∅ x

Tactic:
apply hmn
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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))
⊢ a * b ^ m < a * b ^ (m + 1)

Tactic:
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : 1 < b), 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

Premises used: mul_lt_mul_iff_left, zpow_add_one, HPow.hPow, mul_one
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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

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
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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
⊢ a * b ^ m < a * b ^ (n + 1)

Tactic:
have i1 := hx.1.1.trans_le hx.2.2
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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)
⊢ a * b ^ n < a * b ^ (m + 1)

Tactic:
have i2 := hx.2.1.trans_le hx.1.2
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m ≤ n

Tactic:
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2

Premises used: zpow_lt_zpow_iff_right, mul_lt_mul_iff_left, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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)
i2 : a * b ^ n < a * b ^ (m + 1)
i1₁ : m ≤ n
⊢ n ≤ m

Tactic:
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2

Premises used: zpow_lt_zpow_iff_right, mul_lt_mul_iff_left, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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 : m ≤ n
i2 : n ≤ m
⊢ m = n

Tactic:
le_antisymm i1 i2

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
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 : m ≤ n
i2 : n ≤ m
⊢ m = n

Tactic:
exact le_antisymm i1 i2

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
simp_rw : Pairwise fun (x y : ℤ) ↦ Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
⊢ Pairwise fun (x y : ℤ) ↦ Disjoint (Ico (a * b ^ x) (a * b ^ (x + 1))) (Ico (a * b ^ y) (a * b ^ (y + 1)))

Tactic:
simp_rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
apply : m = n
⊢ Membership.mem (γ := Set α) ∅ x

Tactic:
apply hmn
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ a * b ^ m < a * b ^ (m + 1)

Tactic:
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2