α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n✝ n : ℕ
⊢ StrictMono fun a => a ^ bit1 n
intro a b hab
case inl
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b

case inr
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : 0 ≤ a
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
cases' le_total a 0 with ha ha
case inl.inl
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b

case inl.inr
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
case inl
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
cases' le_or_lt b 0 with hb hb
case inl.inl
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (-b) ^ bit1 n < (-a) ^ bit1 n
case inl.inl
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
rw [← neg_lt_neg_iff, ← neg_pow_bit1, ← neg_pow_bit1]
no goals
case inl.inl
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (-b) ^ bit1 n < (-a) ^ bit1 n
exact pow_lt_pow_of_lt_left (neg_lt_neg hab) (neg_nonneg.2 hb) (bit1_pos (zero_le n))
no goals
case inl.inr
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
exact (pow_bit1_nonpos_iff.2 ha).trans_lt (pow_bit1_pos_iff.2 hb)
no goals
case inr
α : Type ?u.310657
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : 0 ≤ a
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
exact pow_lt_pow_of_lt_left hab ha (bit1_pos (zero_le n))