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

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

Tactic:
have := exists_pow_lt_of_lt_one hb₀ hc₁

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

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred < b
hn : Nat.find this ≠ 0
⊢ False

Tactic:
exact Nat.find_min this (Nat.sub_one_lt hn) H

Result:
no goals

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

Tactic:
by_contra! H

Result:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
⊢ False

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
⊢ Nat.find this ≠ 0

Tactic:
intro hf

Result:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hf : Nat.find this = 0
⊢ False

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hf : Nat.find this = 0
⊢ False

Tactic:
simp only [hf, pow_zero] at H

Result:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
hf : Nat.find this = 0
H : 1 < b * c
⊢ False

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
⊢ False

Tactic:
have hn : Nat.find this ≠ 0 := by
  intro hf
  simp only [hf, pow_zero] at H
  exact (H.trans <| (mul_lt_of_lt_one_right hb₀ hc₁).trans_le hb₁).false

Result:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hn : Nat.find this ≠ 0
⊢ False

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

Tactic:
refine ⟨Nat.find this, h.trans_le ?_, Nat.find_spec this⟩

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

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
hf : Nat.find this = 0
H : 1 < b * c
⊢ False

Tactic:
exact (H.trans <| (mul_lt_of_lt_one_right hb₀ hc₁).trans_le hb₁).false

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hn : Nat.find this ≠ 0
⊢ False

Tactic:
rw [(Nat.succ_pred_eq_of_ne_zero hn).symm, pow_succ, mul_lt_mul_right hc₀] at H

Result:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred < b
hn : Nat.find this ≠ 0
⊢ False