-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ioc_mul_zpow :
    Pairwise (Disjoint on fun n : ℤ => Ioc (a * b ^ n) (a * b ^ (n + 1)))

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n

Tactic:
have i2 := hx.2.1.trans_le hx.1.2

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
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

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
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

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ 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]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise fun x y => Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ioc (a * b ^ n) (a * b ^ (n + 1)))

Tactic:
simp (config := { unfoldPartialApp := true }) only [Function.onFun]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise fun x y => Disjoint (Ioc (a * b ^ x) (a * b ^ (x + 1))) (Ioc (a * b ^ y) (a * b ^ (y + 1)))

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b

Tactic:
rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
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))
⊢ x ∈ ∅

Tactic:
apply hmn

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
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 : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n

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

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise fun x y => Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅

Tactic:
intro m n hmn x hx

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
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))
⊢ x ∈ ∅

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n

Tactic:
have i1 := hx.1.1.trans_le hx.2.2

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
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

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
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