α : Type ?u.308458
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 : ℕ
⊢ a < 0 ∨ a ^ bit1 n = 0 ↔ a < 0 ∨ a = 0
α : Type ?u.308458
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 : ℕ
⊢ a ^ bit1 n ≤ 0 ↔ a ≤ 0
simp only [le_iff_lt_or_eq, pow_bit1_neg_iff]
case refine'_1
α : Type ?u.308458
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 : ℕ
⊢ a < 0 ∨ a ^ bit1 n = 0 → a < 0 ∨ a = 0

case refine'_2
α : Type ?u.308458
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 : ℕ
⊢ a < 0 ∨ a = 0 → a < 0 ∨ a ^ bit1 n = 0
α : Type ?u.308458
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 : ℕ
⊢ a < 0 ∨ a ^ bit1 n = 0 ↔ a < 0 ∨ a = 0
refine' ⟨_, _⟩
case refine'_1.inl
α : Type ?u.308458
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 : ℕ
hpos : a < 0
⊢ a < 0 ∨ a = 0

case refine'_1.inr
α : Type ?u.308458
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 : ℕ
hz : a ^ bit1 n = 0
⊢ a < 0 ∨ a = 0
case refine'_1
α : Type ?u.308458
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 : ℕ
⊢ a < 0 ∨ a ^ bit1 n = 0 → a < 0 ∨ a = 0
rintro (hpos | hz)
case refine'_1.inl.h
α : Type ?u.308458
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 : ℕ
hpos : a < 0
⊢ a < 0
case refine'_1.inl
α : Type ?u.308458
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 : ℕ
hpos : a < 0
⊢ a < 0 ∨ a = 0
left
no goals
case refine'_1.inl.h
α : Type ?u.308458
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 : ℕ
hpos : a < 0
⊢ a < 0
exact hpos
case refine'_1.inr.h
α : Type ?u.308458
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 : ℕ
hz : a ^ bit1 n = 0
⊢ a = 0
case refine'_1.inr
α : Type ?u.308458
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 : ℕ
hz : a ^ bit1 n = 0
⊢ a < 0 ∨ a = 0
right
no goals
case refine'_1.inr.h
α : Type ?u.308458
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 : ℕ
hz : a ^ bit1 n = 0
⊢ a = 0
exact (pow_eq_zero_iff'.1 hz).1
case refine'_2.inl
α : Type ?u.308458
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 : ℕ
hneg : a < 0
⊢ a < 0 ∨ a ^ bit1 n = 0

case refine'_2.inr
α : Type ?u.308458
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 : ℕ
hz : a = 0
⊢ a < 0 ∨ a ^ bit1 n = 0
case refine'_2
α : Type ?u.308458
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 : ℕ
⊢ a < 0 ∨ a = 0 → a < 0 ∨ a ^ bit1 n = 0
rintro (hneg | hz)
case refine'_2.inl.h
α : Type ?u.308458
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 : ℕ
hneg : a < 0
⊢ a < 0
case refine'_2.inl
α : Type ?u.308458
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 : ℕ
hneg : a < 0
⊢ a < 0 ∨ a ^ bit1 n = 0
left
no goals
case refine'_2.inl.h
α : Type ?u.308458
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 : ℕ
hneg : a < 0
⊢ a < 0
exact hneg
case refine'_2.inr.h
α : Type ?u.308458
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 : ℕ
hz : a = 0
⊢ a ^ bit1 n = 0
case refine'_2.inr
α : Type ?u.308458
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 : ℕ
hz : a = 0
⊢ a < 0 ∨ a ^ bit1 n = 0
right
no goals
case refine'_2.inr.h
α : Type ?u.308458
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 : ℕ
hz : a = 0
⊢ a ^ bit1 n = 0
simp [hz, bit1]