-- Mathlib/Algebra/Order/Archimedean/Basic.lean
/-- If `a < b * c`, `b` is positive and `0 < c < 1`, then there is a power `c ^ n` with `n : ℤ`
strictly between `a` and `b`. -/
lemma exists_zpow_btwn_of_lt_mul {a b c : α} (h : a < b * c) (hb₀ : 0 < b) (hc₀ : 0 < c)
    (hc₁ : c < 1) :
    ∃ n : ℤ, a < c ^ n ∧ c ^ n < b

Proof state:
case inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : b ≤ 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn⟩ := exists_pow_btwn_of_lt_mul h hb₀ hb₁ hc₀ hc₁

Result:
case inr.inl.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : b ≤ 1
n : ℕ
hn : a < c ^ n ∧ c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Proof state:
case inr.inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
rcases lt_or_le a 1 with ha₁ | ha₁

Result:
case inr.inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

case inr.inr.inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Proof state:
case inr.inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < c ^ 0 ∧ c ^ 0 < b

Tactic:
rw [zpow_zero]

Result:
case inr.inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < 1 ∧ 1 < b

Proof state:
case inr.inr.inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]

Result:
case inr.inr.inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Proof state:
case inr.inr.inr.intro.intro.refine_1
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ a < c ^ (-↑n)

Tactic:
rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂

Result:
no goals

Proof state:
case inr.inr.inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
refine ⟨-n, ?_, ?_⟩

Result:
case inr.inr.inr.intro.intro.refine_1
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ a < c ^ (-↑n)

case inr.inr.inr.intro.intro.refine_2
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b

Proof state:
case inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
rcases le_or_lt b 1 with hb₁ | hb₁

Result:
case inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : b ≤ 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

case inr.inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Proof state:
case inl.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
n : ℕ
hn : c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
exact ⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩

Result:
no goals

Proof state:
case inr.inr.inr.intro.intro.refine_2
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b

Tactic:
rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ b⁻¹ < a⁻¹ * c

Tactic:
rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁

Result:
case inl.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
n : ℕ
hn : c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Proof state:
case inr.inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
refine ⟨0, ?_⟩

Result:
case inr.inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < c ^ 0 ∧ c ^ 0 < b

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
rcases le_or_lt a 0 with ha | ha

Result:
case inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

case inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Proof state:
case inr.inl.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : b ≤ 1
n : ℕ
hn : a < c ^ n ∧ c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
exact ⟨n, mod_cast hn⟩

Result:
no goals