case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : a < 1
⊢ Injective ((fun x x_1 => x ^ x_1) a)

case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : 1 < a
⊢ Injective ((fun x x_1 => x ^ x_1) a)
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
⊢ Injective ((fun x x_1 => x ^ x_1) a)
rcases h₁.lt_or_lt with (H | H)
no goals
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : a < 1
⊢ Injective ((fun x x_1 => x ^ x_1) a)
exact (zpow_strictAnti h₀ H).injective
no goals
case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : 1 < a
⊢ Injective ((fun x x_1 => x ^ x_1) a)
exact (zpow_strictMono H).injective