[GOAL]
⊢ LinearOrderedAddCommGroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑(natAbs n) = ↑|n|
[PROOFSTEP]
rw [← coe_natAbs, Int.cast_ofNat]
[GOAL]
a : ℤ
⊢ natAbs |a| = natAbs a
[PROOFSTEP]
rw [abs_eq_natAbs]
[GOAL]
a : ℤ
⊢ natAbs ↑(natAbs a) = natAbs a
[PROOFSTEP]
rfl
[GOAL]
a : ℤ
⊢ sign a * |a| = a
[PROOFSTEP]
rw [abs_eq_natAbs, sign_mul_natAbs a]
[GOAL]
n : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {m n : ℤ}, sign m = sign n → sign (m + n) = sign n
[PROOFSTEP]
have : (1 : ℤ) ≠ -1 := by decide
[GOAL]
⊢ 1 ≠ -1
[PROOFSTEP]
decide
[GOAL]
this : 1 ≠ -1
⊢ ∀ {m n : ℤ}, sign m = sign n → sign (m + n) = sign n
[PROOFSTEP]
rintro ((_ | m) | m) ((_ | n) | n)
[GOAL]
case ofNat.zero.ofNat.zero
this : 1 ≠ -1
⊢ sign (ofNat zero) = sign (ofNat zero) → sign (ofNat zero + ofNat zero) = sign (ofNat zero)
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.zero.ofNat.succ
this : 1 ≠ -1
n : ℕ
⊢ sign (ofNat zero) = sign (ofNat (Nat.succ n)) → sign (ofNat zero + ofNat (Nat.succ n)) = sign (ofNat (Nat.succ n))
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.zero.negSucc
this : 1 ≠ -1
n : ℕ
⊢ sign (ofNat zero) = sign -[n+1] → sign (ofNat zero + -[n+1]) = sign -[n+1]
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.ofNat.zero
this : 1 ≠ -1
m : ℕ
⊢ sign (ofNat (Nat.succ m)) = sign (ofNat zero) → sign (ofNat (Nat.succ m) + ofNat zero) = sign (ofNat zero)
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign (ofNat (Nat.succ m)) = sign (ofNat (Nat.succ n)) →
    sign (ofNat (Nat.succ m) + ofNat (Nat.succ n)) = sign (ofNat (Nat.succ n))
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.negSucc
this : 1 ≠ -1
m n : ℕ
⊢ sign (ofNat (Nat.succ m)) = sign -[n+1] → sign (ofNat (Nat.succ m) + -[n+1]) = sign -[n+1]
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case negSucc.ofNat.zero
this : 1 ≠ -1
m : ℕ
⊢ sign -[m+1] = sign (ofNat zero) → sign (-[m+1] + ofNat zero) = sign (ofNat zero)
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case negSucc.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign -[m+1] = sign (ofNat (Nat.succ n)) → sign (-[m+1] + ofNat (Nat.succ n)) = sign (ofNat (Nat.succ n))
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case negSucc.negSucc
this : 1 ≠ -1
m n : ℕ
⊢ sign -[m+1] = sign -[n+1] → sign (-[m+1] + -[n+1]) = sign -[n+1]
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign (↑m + 1 + (↑n + 1)) = 1
[PROOFSTEP]
rw [Int.sign_eq_one_iff_pos]
[GOAL]
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑m + 1 + (↑n + 1)
[PROOFSTEP]
apply Int.add_pos
[GOAL]
case ofNat.succ.ofNat.succ.ha
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑m + 1
[PROOFSTEP]
exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)
[GOAL]
case ofNat.succ.ofNat.succ.hb
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑n + 1
[PROOFSTEP]
exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)
[GOAL]
a : ℤ
a0 : |a| < 1
⊢ a = 0
[PROOFSTEP]
let ⟨hn, hp⟩ := abs_lt.mp a0
[GOAL]
a : ℤ
a0 : |a| < 1
hn : -1 < a
hp : a < 1
⊢ a = 0
[PROOFSTEP]
rw [← zero_add 1, lt_add_one_iff] at hp
[GOAL]
a : ℤ
a0 : |a| < 1
hn : -1 < a
hp✝ : a < 1
hp : a ≤ 0
⊢ a = 0
[PROOFSTEP]
exact hp.antisymm hn
[GOAL]
a : ℤ
⊢ |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1
[PROOFSTEP]
rw [le_iff_lt_or_eq, abs_lt_one_iff, abs_eq (zero_le_one' ℤ)]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C b = C (b + ↑0)
[PROOFSTEP]
erw [add_zero]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + ↑n + 1) = C (b + ↑(n + 1))
[PROOFSTEP]
rw [add_assoc]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + (↑n + 1)) = C (b + ↑(n + 1))
[PROOFSTEP]
rfl
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + -[n + 1+1])
[PROOFSTEP]
refine _root_.cast (by rw [add_sub_assoc]; rfl) (Hp _ (Int.le_of_lt ?_) (neg n))
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + -[n+1] - 1) = C (b + -[n + 1+1])
[PROOFSTEP]
rw [add_sub_assoc]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + (-[n+1] - 1)) = C (b + -[n + 1+1])
[PROOFSTEP]
rfl
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ b + -[n+1] < b
[PROOFSTEP]
conv => rhs; apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b + -[n+1] < b
[PROOFSTEP]
rhs; apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b + -[n+1] < b
[PROOFSTEP]
rhs; apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b + -[n+1] < b
[PROOFSTEP]
rhs
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b
[PROOFSTEP]
apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ b + -[n+1] < b + 0
[PROOFSTEP]
rw [Int.add_lt_add_iff_left]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ -[n+1] < 0
[PROOFSTEP]
apply negSucc_lt_zero
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C z
[PROOFSTEP]
rw [← sub_add_cancel (G := ℤ) z b, add_comm]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C (b + (z - b))
[PROOFSTEP]
exact
  match z - b with
  | .ofNat n => pos n
  | .negSucc n => neg n
[GOAL]
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ m ≤ n → P n
[PROOFSTEP]
refine Int.inductionOn' n m ?_ ?_ ?_
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ m ≤ m → P m
[PROOFSTEP]
intro
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
a✝ : m ≤ m
⊢ P m
[PROOFSTEP]
exact h0
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), m ≤ k → (m ≤ k → P k) → m ≤ k + 1 → P (k + 1)
[PROOFSTEP]
intro k hle hi _
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : m ≤ k
hi : m ≤ k → P k
a✝ : m ≤ k + 1
⊢ P (k + 1)
[PROOFSTEP]
exact h1 k hle (hi hle)
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), k ≤ m → (m ≤ k → P k) → m ≤ k - 1 → P (k - 1)
[PROOFSTEP]
intro k hle _ hle'
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ P (k - 1)
[PROOFSTEP]
exfalso
[GOAL]
case refine_3.h
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ False
[PROOFSTEP]
exact lt_irrefl k (le_sub_one_iff.mp (hle.trans hle'))
[GOAL]
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ n ≤ m → P n
[PROOFSTEP]
refine Int.inductionOn' n m ?_ ?_ ?_
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ m ≤ m → P m
[PROOFSTEP]
intro
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
a✝ : m ≤ m
⊢ P m
[PROOFSTEP]
exact h0
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ ∀ (k : ℤ), m ≤ k → (k ≤ m → P k) → k + 1 ≤ m → P (k + 1)
[PROOFSTEP]
intro k hle _ hle'
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n k : ℤ
hle : m ≤ k
a✝ : k ≤ m → P k
hle' : k + 1 ≤ m
⊢ P (k + 1)
[PROOFSTEP]
exfalso
[GOAL]
case refine_2.h
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n k : ℤ
hle : m ≤ k
a✝ : k ≤ m → P k
hle' : k + 1 ≤ m
⊢ False
[PROOFSTEP]
exact lt_irrefl k (add_one_le_iff.mp (hle'.trans hle))
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ ∀ (k : ℤ), k ≤ m → (k ≤ m → P k) → k - 1 ≤ m → P (k - 1)
[PROOFSTEP]
intro k hle hi _
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n k : ℤ
hle : k ≤ m
hi : k ≤ m → P k
a✝ : k - 1 ≤ m
⊢ P (k - 1)
[PROOFSTEP]
exact h1 k hle (hi hle)
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑(natAbs -[n+1])
⊢ -(a / -[n+1]) = -0
[PROOFSTEP]
rw [← Int.ediv_neg]
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑(natAbs -[n+1])
⊢ a / - -[n+1] = -0
[PROOFSTEP]
exact ediv_eq_zero_of_lt H1 H2
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ a % b < |b|
[PROOFSTEP]
rw [← emod_abs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|
[PROOFSTEP]
exact emod_lt_of_pos _ (abs_pos.2 H)
[GOAL]
a b : ℤ
n✝ : ℕ
m n k i : ℤ
H : m % n = k % n
⊢ (m + i) % n = (k + i) % n
[PROOFSTEP]
rw [← emod_add_emod, ← emod_add_emod k, H]
[GOAL]
a b : ℤ
n : ℕ
i : ℤ
⊢ -i % 2 = i % 2
[PROOFSTEP]
apply Int.emod_eq_emod_iff_emod_sub_eq_zero.mpr
[GOAL]
a b : ℤ
n : ℕ
i : ℤ
⊢ (-i - i) % 2 = 0
[PROOFSTEP]
convert Int.mul_emod_right 2 (-i) using 2
[GOAL]
case h.e'_2.h.e'_5
a b : ℤ
n : ℕ
i : ℤ
⊢ -i - i = 2 * -i
[PROOFSTEP]
rw [two_mul, sub_eq_add_neg]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|
[PROOFSTEP]
rw [abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ ↑(natAbs (a / ↑n)) ≤ ↑(natAbs a)
[PROOFSTEP]
exact
  ofNat_le_ofNat_of_le
    (match a, n with
    | (m : ℕ), n => Nat.div_le_self _ _
    | -[m+1], 0 => Nat.zero_le _
    | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|
[PROOFSTEP]
rw [Int.ediv_neg, abs_neg]
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|
[PROOFSTEP]
apply this
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ 0 ≤ 2
[PROOFSTEP]
decide
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ |2| ≠ 0
[PROOFSTEP]
decide
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
⊢ 2 ≠ 0
[PROOFSTEP]
decide
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
h₁✝ : 0 ≤ n % 2
k : ℕ
h₁ : ↑(k + 2) < 2
x✝ : 0 ≤ ↑(k + 2)
⊢ 2 ≤ ↑(k + 2)
[PROOFSTEP]
rw [Nat.cast_add]
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
h₁✝ : 0 ≤ n % 2
k : ℕ
h₁ : ↑(k + 2) < 2
x✝ : 0 ≤ ↑(k + 2)
⊢ 2 ≤ ↑k + ↑2
[PROOFSTEP]
exact (le_add_iff_nonneg_left 2).2 (NonNeg.mk k)
[GOAL]
a✝ b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
h₁✝ : 0 ≤ n % 2
a : ℕ
x✝ : -[a+1] < 2
h₁ : 0 ≤ -[a+1]
⊢ -[a+1] = 0 ∨ -[a+1] = 1
[PROOFSTEP]
cases h₁
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : a = 0
⊢ a * b / a ∣ a * b * c / a
[PROOFSTEP]
simp [az]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : ¬a = 0
⊢ a * b / a ∣ a * b * c / a
[PROOFSTEP]
rw [Int.mul_ediv_cancel_left _ az, mul_assoc, Int.mul_ediv_cancel_left _ az]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : ¬a = 0
⊢ b ∣ b * c
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
a b : ℤ
n : ℕ
z : ℤ
hz : z ≠ 0
⊢ |sign z| = 1
[PROOFSTEP]
rw [abs_eq_natAbs, natAbs_sign_of_nonzero hz, Int.ofNat_one]
[GOAL]
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) → ¬n ∣ m
[PROOFSTEP]
rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩
[GOAL]
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : n * k < n * l
h2k : n * l < n * (k + 1)
⊢ False
[PROOFSTEP]
rw [mul_lt_mul_left hn] at h1k h2k
[GOAL]
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : l < k + 1
⊢ False
[PROOFSTEP]
rw [lt_add_one_iff, ← not_lt] at h2k
[GOAL]
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : ¬k < l
⊢ False
[PROOFSTEP]
exact h2k h1k
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ ¬n ∣ m → ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
intro h
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : ¬n ∣ m
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
rw [dvd_iff_emod_eq_zero, ← Ne.def] at h
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
have := (emod_nonneg m hn.ne.symm).lt_of_ne h.symm
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
simp (config := { singlePass := true }) only [← emod_add_ediv m n]
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m % n + n * (m / n) ∧ m % n + n * (m / n) < n * (k + 1)
[PROOFSTEP]
refine' ⟨m / n, lt_add_of_pos_left _ this, _⟩
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n * (m / n + 1)
[PROOFSTEP]
rw [add_comm _ (1 : ℤ), left_distrib, mul_one]
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n + n * (m / n)
[PROOFSTEP]
exact add_lt_add_right (emod_lt_of_pos _ hn) _
[GOAL]
a✝ b : ℤ
n : ℕ
a : ℤ
az : a = 0
⊢ sign a = a / |a|
[PROOFSTEP]
simp [az]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ 0 ≤ a - a / b * b
[PROOFSTEP]
rw [mul_comm, ← emod_def]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ 0 ≤ a % b
[PROOFSTEP]
apply emod_nonneg _ H
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a ≤ c * b
[PROOFSTEP]
rw [← Int.ediv_mul_cancel H2]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a / b * b ≤ c * b
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right H3 H1
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H1 : 0 < a
H2 : 0 ≤ b
H3 : b ∣ a
⊢ 0 * b < a
[PROOFSTEP]
rwa [zero_mul]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c d : ℤ
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * (c / d)
[PROOFSTEP]
rw [← Int.mul_ediv_assoc _ H2]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c d : ℤ
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * c / d
[PROOFSTEP]
exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm
[GOAL]
a b : ℤ
n : ℕ
s t : ℤ
hst : s ∣ t
⊢ t / s ∣ t
[PROOFSTEP]
rcases eq_or_ne s 0 with (rfl | hs)
[GOAL]
case inl
a b : ℤ
n : ℕ
t : ℤ
hst : 0 ∣ t
⊢ t / 0 ∣ t
[PROOFSTEP]
simpa using hst
[GOAL]
case inr
a b : ℤ
n : ℕ
s t : ℤ
hst : s ∣ t
hs : s ≠ 0
⊢ t / s ∣ t
[PROOFSTEP]
rcases hst with ⟨c, hc⟩
[GOAL]
case inr.intro
a b : ℤ
n : ℕ
s t : ℤ
hs : s ≠ 0
c : ℤ
hc : t = s * c
⊢ t / s ∣ t
[PROOFSTEP]
simp [hc, Int.mul_ediv_cancel_left _ hs]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ toNat a ≤ n ↔ a ≤ ↑n
[PROOFSTEP]
rw [ofNat_le.symm, toNat_eq_max, max_le_iff]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ a ≤ ↑n ∧ 0 ≤ ↑n ↔ a ≤ ↑n
[PROOFSTEP]
exact and_iff_left (ofNat_zero_le _)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
h : a ≤ b
⊢ toNat a ≤ toNat b
[PROOFSTEP]
rw [toNat_le]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
h : a ≤ b
⊢ a ≤ ↑(toNat b)
[PROOFSTEP]
exact le_trans h (self_le_toNat b)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
hb : 0 < b
h : toNat a < toNat b
⊢ a < b
[PROOFSTEP]
cases a
[GOAL]
case ofNat
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : toNat (ofNat a✝) < toNat b
⊢ ofNat a✝ < b
case negSucc a b✝ : ℤ n : ℕ b : ℤ hb : 0 < b a✝ : ℕ h : toNat -[a✝+1] < toNat b ⊢ -[a✝+1] < b
[PROOFSTEP]
exact lt_toNat.1 h
[GOAL]
case negSucc
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : toNat -[a✝+1] < toNat b
⊢ -[a✝+1] < b
[PROOFSTEP]
exact lt_trans (neg_of_sign_eq_neg_one rfl) hb
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
hb : 0 < b
h : a < b
⊢ toNat a < toNat b
[PROOFSTEP]
rw [lt_toNat]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
hb : 0 < b
h : a < b
⊢ ↑(toNat a) < b
[PROOFSTEP]
cases a
[GOAL]
case ofNat
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : ofNat a✝ < b
⊢ ↑(toNat (ofNat a✝)) < b
case negSucc a b✝ : ℤ n : ℕ b : ℤ hb : 0 < b a✝ : ℕ h : -[a✝+1] < b ⊢ ↑(toNat -[a✝+1]) < b
[PROOFSTEP]
exact h
[GOAL]
case negSucc
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : -[a✝+1] < b
⊢ ↑(toNat -[a✝+1]) < b
[PROOFSTEP]
exact hb
[GOAL]
a b : ℤ
n : ℕ
i : ℤ
h : 0 < i
⊢ ↑(toNat i - 1) = i - 1
[PROOFSTEP]
simp [h, le_of_lt h, push_cast]


[GOAL]
m n : ℕ
⊢ ↑m - ↑n ≤ ↑(m - n)
[PROOFSTEP]
by_cases h : m ≥ n
[GOAL]
case pos
m n : ℕ
h : m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)
[PROOFSTEP]
exact le_of_eq (Int.ofNat_sub h).symm
[GOAL]
case neg
m n : ℕ
h : ¬m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)
[PROOFSTEP]
simp [le_of_not_ge h, ofNat_le]
[GOAL]
n : ℕ
⊢ 0 ≤ ↑n
[PROOFSTEP]
simp
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ a * a = b * b
[PROOFSTEP]
exact natAbs_eq_iff_mul_self_eq
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ a * a < b * b
[PROOFSTEP]
exact natAbs_lt_iff_mul_self_lt
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ a * a ≤ b * b
[PROOFSTEP]
exact natAbs_le_iff_mul_self_le
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ natAbs a = natAbs b ↔ a = b
[PROOFSTEP]
rw [← sq_eq_sq ha hb, ← natAbs_eq_iff_sq_eq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ natAbs a = natAbs b ↔ a = b
[PROOFSTEP]
simpa only [Int.natAbs_neg, neg_inj] using
  natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) (neg_nonneg_of_nonpos hb)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ natAbs a = natAbs b ↔ a = -b
[PROOFSTEP]
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg ha (neg_nonneg_of_nonpos hb)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ natAbs a = natAbs b ↔ -a = b
[PROOFSTEP]
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) hb
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a : ℤ
x✝ : a ∈ Iic 0
b : ℤ
hb : b ∈ Iic 0
hab : a < b
⊢ natAbs b < natAbs a
[PROOFSTEP]
simpa [Int.natAbs_neg] using natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)
[GOAL]
a b : ℤ
n✝ n : ℕ
h : ↑(n + 1) ≤ 0
⊢ 0 < ↑(n + 1)
[PROOFSTEP]
simp
[GOAL]
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ div2 (bit b n) = n
[PROOFSTEP]
rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]
[GOAL]
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0
case H a b✝ : ℤ n✝ : ℕ b : Bool n : ℤ ⊢ 2 ≠ 0
[PROOFSTEP]
cases b
[GOAL]
case false
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0
[PROOFSTEP]
simp
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0
[PROOFSTEP]
show ofNat _ = _
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ ofNat (1 / 2) = 0
[PROOFSTEP]
rw [Nat.div_eq_zero]
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ ofNat 0 = 0
[PROOFSTEP]
simp
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ 1 < 2
[PROOFSTEP]
simp
[GOAL]
case H
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ 2 ≠ 0
[PROOFSTEP]
decide


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Mul α
s t u : Set α
a : α
⊢ op '' s • t = t * s
[PROOFSTEP]
rw [← image2_smul, ← image2_mul, image2_image_left, image2_swap]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Mul α
s t u : Set α
a : α
⊢ image2 (fun a b => SMul.smul (op b) a) t s = image2 (fun x x_1 => x * x_1) t s
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b✝ : β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
T : Set γ
⊢ (a • b) • T = a • b • T
[PROOFSTEP]
simp only [← image_smul, image_image, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun x => 1 • x) '' s = s
[PROOFSTEP]
simp_rw [one_smul, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
⊢ ∀ (b : Set β), 1 • b = b
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
b✝ : Set β
⊢ 1 • b✝ = b✝
[PROOFSTEP]
simp only [← image_smul, one_smul, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
⊢ ∀ (x y : α) (b : Set β), (x * y) • b = x • y • b
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
x✝ y✝ : α
b✝ : Set β
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
[PROOFSTEP]
simp only [← image_smul, image_image, ← mul_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ {x✝ • 0} = 0
[PROOFSTEP]
rw [smul_zero, singleton_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {x✝ • 1} = 1
[PROOFSTEP]
rw [smul_one, singleton_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
⊢ s = 0 ∨ t = 0
[PROOFSTEP]
by_contra' H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
H : s ≠ 0 ∧ t ≠ 0
⊢ False
[PROOFSTEP]
have hst : (s • t).Nonempty := h.symm.subst zero_nonempty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
H : s ≠ 0 ∧ t ≠ 0
hst : Set.Nonempty (s • t)
⊢ False
[PROOFSTEP]
rw [Ne.def, ← hst.of_smul_left.subset_zero_iff, Ne.def, ← hst.of_smul_right.subset_zero_iff] at H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
hst : Set.Nonempty (s • t)
⊢ False
[PROOFSTEP]
simp only [not_subset, mem_zero] at H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
hst : Set.Nonempty (s • t)
H : (∃ a, a ∈ s ∧ ¬a = 0) ∧ ∃ a, a ∈ t ∧ ¬a = 0
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
[GOAL]
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a✝ : α
b✝ : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
hst : Set.Nonempty (s • t)
a : α
hs : a ∈ s
ha : ¬a = 0
b : β
ht : b ∈ t
hb : ¬b = 0
⊢ False
[PROOFSTEP]
exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul hs ht).elim ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
⊢ a = 0 ∨ s = 0
[PROOFSTEP]
by_contra' H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
H : a ≠ 0 ∧ s ≠ 0
⊢ False
[PROOFSTEP]
have hst : (a • s).Nonempty := h.symm.subst zero_nonempty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
H : a ≠ 0 ∧ s ≠ 0
hst : Set.Nonempty (a • s)
⊢ False
[PROOFSTEP]
rw [Ne.def, Ne.def, ← hst.of_image.subset_zero_iff, not_subset] at H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
H : ¬a = 0 ∧ ∃ a, a ∈ s ∧ ¬a ∈ 0
hst : Set.Nonempty (a • s)
⊢ False
[PROOFSTEP]
obtain ⟨ha, b, ht, hb⟩ := H
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b✝ : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
hst : Set.Nonempty (a • s)
ha : ¬a = 0
b : β
ht : b ∈ s
hb : ¬b ∈ 0
⊢ False
[PROOFSTEP]
exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul_set ht).elim ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x✝ : γ
⊢ x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t
[PROOFSTEP]
simp [mem_smul, mem_smul_set, h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s✝ : Set α
t : Set β
s : Set α
⊢ s • 0 ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Set α
t✝ t : Set β
⊢ 0 • t ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Set α
t : Set β
hs : Set.Nonempty s
⊢ 0 ⊆ s • 0
[PROOFSTEP]
simpa [mem_smul] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Set α
t : Set β
ht : Set.Nonempty t
⊢ 0 ⊆ 0 • t
[PROOFSTEP]
simpa [mem_smul] using ht
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s✝ : Set α
t s : Set β
h : Set.Nonempty s
⊢ 0 • s = 0
[PROOFSTEP]
simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s • t → 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
rintro ⟨a, b, ha, hb, h⟩
[GOAL]
case mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a✝ a : α
b : β
ha : a ∈ s
hb : b ∈ t
h : (fun x x_1 => x • x_1) a b = 0
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
obtain rfl | rfl := eq_zero_or_eq_zero_of_smul_eq_zero h
[GOAL]
case mp.intro.intro.intro.intro.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
b : β
hb : b ∈ t
ha : 0 ∈ s
h : (fun x x_1 => x • x_1) 0 b = 0
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
exact Or.inl ⟨ha, b, hb⟩
[GOAL]
case mp.intro.intro.intro.intro.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a✝ a : α
ha : a ∈ s
hb : 0 ∈ t
h : (fun x x_1 => x • x_1) a 0 = 0
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
exact Or.inr ⟨hb, a, ha⟩
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s → 0 ∈ s • t
[PROOFSTEP]
rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
[GOAL]
case mpr.inl.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
hs : 0 ∈ s
b : β
hb : b ∈ t
⊢ 0 ∈ s • t
[PROOFSTEP]
exact ⟨0, b, hs, hb, zero_smul _ _⟩
[GOAL]
case mpr.inr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a✝ : α
ht : 0 ∈ t
a : α
ha : a ∈ s
⊢ 0 ∈ s • t
[PROOFSTEP]
exact ⟨a, 0, ha, ht, smul_zero _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t
[PROOFSTEP]
refine' ⟨_, zero_mem_smul_set⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t
[PROOFSTEP]
rintro ⟨b, hb, h⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x => a • x) b = 0
⊢ 0 ∈ t
[PROOFSTEP]
rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s t A B : Set β
a : α
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A
[PROOFSTEP]
simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
rw [← nonempty_iff_ne_empty]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ Set.Nonempty (x • s ∩ t) ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ Set.Nonempty (x • s ∩ t) → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
rintro ⟨a, h, ha⟩
[GOAL]
case mp.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
[GOAL]
case mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ x • b * b⁻¹ = x
[PROOFSTEP]
simp
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x : β
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ Set.Nonempty ((a * b⁻¹) • s ∩ t)
[PROOFSTEP]
exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x : β
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ (a * b⁻¹) • b = a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
[PROOFSTEP]
simp_rw [smul_inter_ne_empty_iff, div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
rw [← nonempty_iff_ne_empty]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ Set.Nonempty (x • s ∩ t) ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ Set.Nonempty (x • s ∩ t) → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
rintro ⟨a, h, ha⟩
[GOAL]
case mp.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
[GOAL]
case mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ b⁻¹ * x • b = unop x
[PROOFSTEP]
simp
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, hb⟩, H⟩
[GOAL]
case mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
⊢ Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
[GOAL]
case mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ x • a = b
[PROOFSTEP]
simp [← this]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t A B : Set β
a : α
x : β
s : Set β
⊢ ⋃ (g : α), g • s = {a | ∃ g, g • a ∈ s}
[PROOFSTEP]
simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
s : Set α
t : Set β
⊢ a • -t = -(a • t)
[PROOFSTEP]
simp_rw [← image_smul, ← image_neg, image_image, smul_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
s : Set α
t : Set β
⊢ s • -t = -(s • t)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
s : Set α
t : Set β
⊢ s • Neg.neg '' t = Neg.neg '' (s • t)
[PROOFSTEP]
exact image_image2_right_comm smul_neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
⊢ (a + b) • s ⊆ a • s + b • s
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x => (a + b) • x) x ∈ a • s + b • s
[PROOFSTEP]
simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ -a • t = -(a • t)
[PROOFSTEP]
simp_rw [← image_smul, ← image_neg, image_image, neg_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ -s • t = -(s • t)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ Neg.neg '' s • t = Neg.neg '' (s • t)
[PROOFSTEP]
exact image2_image_left_comm neg_smul


[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝² : DecidablePred (r a)
inst✝¹ : (a : α) → Decidable (r a b)
m n : ℕ
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∑ a in s, card (bipartiteAbove r t a) = ∑ b in t, card (bipartiteBelow r s b)
[PROOFSTEP]
simp_rw [card_eq_sum_ones, bipartiteAbove, bipartiteBelow, sum_filter]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝² : DecidablePred (r a)
inst✝¹ : (a : α) → Decidable (r a b)
m n : ℕ
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ (∑ x in s, ∑ a in t, if r x a then 1 else 0) = ∑ x in t, ∑ a in s, if r a x then 1 else 0
[PROOFSTEP]
exact sum_comm
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
⊢ card s ≤ card t
[PROOFSTEP]
classical
rw [← mul_one s.card, ← mul_one t.card]
exact
  card_mul_le_card_mul r
    (fun a h ↦
      card_pos.2
        (by
          rw [← coe_nonempty, coe_bipartiteAbove]
          exact hs _ h : (t.bipartiteAbove r a).Nonempty))
    (fun b h ↦
      card_le_one.2
        (by
          simp_rw [mem_bipartiteBelow]
          exact ht _ h))
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
⊢ card s ≤ card t
[PROOFSTEP]
rw [← mul_one s.card, ← mul_one t.card]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
⊢ card s * 1 ≤ card t * 1
[PROOFSTEP]
exact
  card_mul_le_card_mul r
    (fun a h ↦
      card_pos.2
        (by
          rw [← coe_nonempty, coe_bipartiteAbove]
          exact hs _ h : (t.bipartiteAbove r a).Nonempty))
    (fun b h ↦
      card_le_one.2
        (by
          simp_rw [mem_bipartiteBelow]
          exact ht _ h))
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a✝ a' : α
b b' : β
inst✝¹ : DecidablePred (r a✝)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
a : α
h : a ∈ s
⊢ Finset.Nonempty (bipartiteAbove r t a)
[PROOFSTEP]
rw [← coe_nonempty, coe_bipartiteAbove]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a✝ a' : α
b b' : β
inst✝¹ : DecidablePred (r a✝)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
a : α
h : a ∈ s
⊢ Set.Nonempty {b | b ∈ t ∧ r a b}
[PROOFSTEP]
exact hs _ h
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b✝ b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b✝)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ bipartiteBelow r s b → ∀ (b_1 : α), b_1 ∈ bipartiteBelow r s b → a = b_1
[PROOFSTEP]
simp_rw [mem_bipartiteBelow]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b✝ b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b✝)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1
[PROOFSTEP]
exact ht _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : LeftTotal r
h₂ : LeftUnique r
⊢ ∀ (a : α), a ∈ univ → ∃ b, b ∈ univ ∧ r a b
[PROOFSTEP]
simpa using h₁
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : RightTotal r
h₂ : RightUnique r
⊢ ∀ (b : β), b ∈ univ → ∃ a, a ∈ univ ∧ r a b
[PROOFSTEP]
simpa using h₁


[GOAL]
m n r : ℤ
⊢ r ∈ range m n ↔ m ≤ r ∧ r < n
[PROOFSTEP]
simp only [range, List.mem_map, List.mem_range, lt_toNat, lt_sub_iff_add_lt, add_comm]
[GOAL]
m n r : ℤ
⊢ (∃ a, m + ↑a < n ∧ m + ↑a = r) ↔ m ≤ r ∧ r < n
[PROOFSTEP]
exact
  ⟨fun ⟨a, ha⟩ => ha.2 ▸ ⟨le_add_of_nonneg_right (Int.coe_nat_nonneg _), ha.1⟩, fun h =>
    ⟨toNat (r - m), by simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]⟩⟩
[GOAL]
m n r : ℤ
h : m ≤ r ∧ r < n
⊢ m + ↑(toNat (r - m)) < n ∧ m + ↑(toNat (r - m)) = r
[PROOFSTEP]
simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ range m n → P r) ↔ ∀ (r : ℤ), m ≤ r → r < n → P r
[PROOFSTEP]
simp only [mem_range_iff, and_imp]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ Decidable (∀ (r : ℤ), m ≤ r → r ≤ n → P r)
[PROOFSTEP]
apply decidable_of_iff (∀ r ∈ range m (n + 1), P r)
[GOAL]
case h
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ range m (n + 1) → P r) ↔ ∀ (r : ℤ), m ≤ r → r ≤ n → P r
[PROOFSTEP]
apply Iff.intro
[GOAL]
case h.mp
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ range m (n + 1) → P r) → ∀ (r : ℤ), m ≤ r → r ≤ n → P r
[PROOFSTEP]
intros h _ _
[GOAL]
case h.mpr
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), m ≤ r → r ≤ n → P r) → ∀ (r : ℤ), r ∈ range m (n + 1) → P r
[PROOFSTEP]
intros h _ _
[GOAL]
case h.mp
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), r ∈ range m (n + 1) → P r
r✝ : ℤ
a✝ : m ≤ r✝
⊢ r✝ ≤ n → P r✝
[PROOFSTEP]
intro _
[GOAL]
case h.mp
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), r ∈ range m (n + 1) → P r
r✝ : ℤ
a✝¹ : m ≤ r✝
a✝ : r✝ ≤ n
⊢ P r✝
[PROOFSTEP]
apply h
[GOAL]
case h.mp.a
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), r ∈ range m (n + 1) → P r
r✝ : ℤ
a✝¹ : m ≤ r✝
a✝ : r✝ ≤ n
⊢ r✝ ∈ range m (n + 1)
[PROOFSTEP]
simp_all only [mem_range_iff, and_imp, lt_add_one_iff]
[GOAL]
case h.mpr
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), m ≤ r → r ≤ n → P r
r✝ : ℤ
a✝ : r✝ ∈ range m (n + 1)
⊢ P r✝
[PROOFSTEP]
simp_all only [mem_range_iff, and_imp, lt_add_one_iff]


[GOAL]
m n : ℕ
⊢ bodd (subNatNat m n) = xor (Nat.bodd m) (Nat.bodd n)
[PROOFSTEP]
apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd
[GOAL]
case hp
m n : ℕ
⊢ ∀ (i n : ℕ), bodd ↑i = xor (Nat.bodd (n + i)) (Nat.bodd n)
[PROOFSTEP]
intros i j
[GOAL]
case hn
m n : ℕ
⊢ ∀ (i m : ℕ), bodd -[i+1] = xor (Nat.bodd m) (Nat.bodd (m + i + 1))
[PROOFSTEP]
intros i j
[GOAL]
case hp
m n i j : ℕ
⊢ bodd ↑i = xor (Nat.bodd (j + i)) (Nat.bodd j)
[PROOFSTEP]
simp only [Int.bodd, Int.bodd_coe, Nat.bodd_add]
[GOAL]
case hn
m n i j : ℕ
⊢ bodd -[i+1] = xor (Nat.bodd j) (Nat.bodd (j + i + 1))
[PROOFSTEP]
simp only [Int.bodd, Int.bodd_coe, Nat.bodd_add]
[GOAL]
case hp
m n i j : ℕ
⊢ Nat.bodd i = xor (xor (Nat.bodd j) (Nat.bodd i)) (Nat.bodd j)
[PROOFSTEP]
cases Nat.bodd i
[GOAL]
case hn
m n i j : ℕ
⊢ (!Nat.bodd i) = xor (Nat.bodd j) (xor (xor (Nat.bodd j) (Nat.bodd i)) (Nat.bodd 1))
[PROOFSTEP]
cases Nat.bodd i
[GOAL]
case hp.false
m n i j : ℕ
⊢ false = xor (xor (Nat.bodd j) false) (Nat.bodd j)
[PROOFSTEP]
simp
[GOAL]
case hp.true
m n i j : ℕ
⊢ true = xor (xor (Nat.bodd j) true) (Nat.bodd j)
[PROOFSTEP]
simp
[GOAL]
case hn.false
m n i j : ℕ
⊢ (!false) = xor (Nat.bodd j) (xor (xor (Nat.bodd j) false) (Nat.bodd 1))
[PROOFSTEP]
simp
[GOAL]
case hn.true
m n i j : ℕ
⊢ (!true) = xor (Nat.bodd j) (xor (xor (Nat.bodd j) true) (Nat.bodd 1))
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ bodd (negOfNat n) = Nat.bodd n
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ bodd (negOfNat Nat.zero) = Nat.bodd Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ bodd (negOfNat (Nat.succ n✝)) = Nat.bodd (Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ bodd (negOfNat (Nat.succ n✝)) = !Nat.bodd n✝
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
⊢ bodd (-n) = bodd n
[PROOFSTEP]
cases n with
| ofNat =>
  rw [← negOfNat_eq, bodd_negOfNat]
  simp
| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]
    -- Porting note: Heavily refactored proof, used to work all with `simp`:
    -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
n : ℤ
⊢ bodd (-n) = bodd n
[PROOFSTEP]
cases n with
| ofNat =>
  rw [← negOfNat_eq, bodd_negOfNat]
  simp
| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]
    -- Porting note: Heavily refactored proof, used to work all with `simp`:
    -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
case ofNat
a✝ : ℕ
⊢ bodd (-ofNat a✝) = bodd (ofNat a✝)
[PROOFSTEP]

| ofNat =>
  rw [← negOfNat_eq, bodd_negOfNat]
  simp
[GOAL]
case ofNat
a✝ : ℕ
⊢ bodd (-ofNat a✝) = bodd (ofNat a✝)
[PROOFSTEP]
rw [← negOfNat_eq, bodd_negOfNat]
[GOAL]
case ofNat
a✝ : ℕ
⊢ Nat.bodd a✝ = bodd (ofNat a✝)
[PROOFSTEP]
simp
[GOAL]
case negSucc
n : ℕ
⊢ bodd (- -[n+1]) = bodd -[n+1]
[PROOFSTEP]

| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]
    -- Porting note: Heavily refactored proof, used to work all with `simp`:
    -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
case negSucc
n : ℕ
⊢ bodd (- -[n+1]) = bodd -[n+1]
[PROOFSTEP]
rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
[GOAL]
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = bodd -[n+1]
[PROOFSTEP]
change (!Nat.bodd n) = !(bodd n)
[GOAL]
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = !bodd ↑n
[PROOFSTEP]
rw [bodd_coe]
  -- Porting note: Heavily refactored proof, used to work all with `simp`:
  -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
m n : ℤ
⊢ bodd (m + n) = xor (bodd m) (bodd n)
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
n : ℤ
m : ℕ
⊢ bodd (ofNat m + n) = xor (bodd (ofNat m)) (bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case negSucc
n : ℤ
m : ℕ
⊢ bodd (-[m+1] + n) = xor (bodd -[m+1]) (bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd (ofNat m + ofNat n) = xor (bodd (ofNat m)) (bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ bodd (ofNat m + -[n+1]) = xor (bodd (ofNat m)) (bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ bodd (-[m+1] + ofNat n) = xor (bodd -[m+1]) (bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd (-[m+1] + -[n+1]) = xor (bodd -[m+1]) (bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd (↑m + ↑n) = xor (bodd ↑m) (bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ xor (Nat.bodd m) (Nat.bodd (Nat.succ n)) = xor (bodd ↑m) (bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ xor (Nat.bodd n) (Nat.bodd (Nat.succ m)) = xor (bodd -[m+1]) (bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd -[Nat.succ (m + n)+1] = xor (bodd -[m+1]) (bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ Nat.bodd (Nat.succ (m + n) + 1) = Nat.bodd (m + 1 + (n + 1))
[PROOFSTEP]
rw [← Nat.succ_add, add_assoc]
  -- Porting note: Heavily refactored proof, used to work all with `simp`:
  -- `by cases m with m m; cases n with n n; unfold has_add.add;`
  -- `simp [int.add, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
m n : ℤ
⊢ bodd (m * n) = (bodd m && bodd n)
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
n : ℤ
m : ℕ
⊢ bodd (ofNat m * n) = (bodd (ofNat m) && bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case negSucc
n : ℤ
m : ℕ
⊢ bodd (-[m+1] * n) = (bodd -[m+1] && bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd (ofNat m * ofNat n) = (bodd (ofNat m) && bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ bodd (ofNat m * -[n+1]) = (bodd (ofNat m) && bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ bodd (-[m+1] * ofNat n) = (bodd -[m+1] && bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd (-[m+1] * -[n+1]) = (bodd -[m+1] && bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd ↑(m * n) = (bodd ↑m && bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ bodd (-↑(m * Nat.succ n)) = (bodd ↑m && bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ bodd (-↑(Nat.succ m * n)) = (bodd -[m+1] && bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd ↑(Nat.succ m * Nat.succ n) = (bodd -[m+1] && bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
n : ℕ
⊢ (bif bodd ↑n then 1 else 0) + 2 * div2 ↑n = ↑n
[PROOFSTEP]
rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
[GOAL]
n : ℕ
⊢ (bif bodd ↑n then 1 else 0) = ↑(bif bodd ↑n then 1 else 0)
[PROOFSTEP]
cases bodd n
[GOAL]
case false
n : ℕ
⊢ (bif false then 1 else 0) = ↑(bif false then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (bif true then 1 else 0) = ↑(bif true then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ↑(bif bodd ↑n then 1 else 0) + 2 * div2 ↑n = ↑n
[PROOFSTEP]
exact congr_arg ofNat n.bodd_add_div2
[GOAL]
n : ℕ
⊢ (bif bodd -[n+1] then 1 else 0) + 2 * div2 -[n+1] = -[n+1]
[PROOFSTEP]
refine' Eq.trans _ (congr_arg negSucc n.bodd_add_div2)
[GOAL]
n : ℕ
⊢ (bif bodd -[n+1] then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
dsimp [bodd]
[GOAL]
n : ℕ
⊢ (bif !Nat.bodd n then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
cases Nat.bodd n
[GOAL]
case false
n : ℕ
⊢ (bif !false then 1 else 0) + 2 * div2 -[n+1] = -[(bif false then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
dsimp [cond, not, div2, Int.mul]
[GOAL]
case true
n : ℕ
⊢ (bif !true then 1 else 0) + 2 * div2 -[n+1] = -[(bif true then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
dsimp [cond, not, div2, Int.mul]
[GOAL]
case false
n : ℕ
⊢ 1 + 2 * -[Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]
[PROOFSTEP]
change -[2 * Nat.div2 n+1] = _
[GOAL]
case false
n : ℕ
⊢ -[2 * Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]
[PROOFSTEP]
rw [zero_add]
[GOAL]
case true
n : ℕ
⊢ 0 + 2 * -[Nat.div2 n+1] = -[1 + 2 * Nat.div2 n+1]
[PROOFSTEP]
rw [zero_add, add_comm]
[GOAL]
case true
n : ℕ
⊢ 2 * -[Nat.div2 n+1] = -[2 * Nat.div2 n + 1+1]
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℤ
⊢ bit b n = 2 * n + bif b then 1 else 0
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0
case true n : ℤ ⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply (bit0_val n).trans (add_zero _).symm
[GOAL]
case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply bit1_val
[GOAL]
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C n
[PROOFSTEP]
rw [← bit_decomp n]
[GOAL]
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C (bit (bodd n) (div2 n))
[PROOFSTEP]
apply h
[GOAL]
b : Bool
n : ℕ
⊢ bit b ↑n = ↑(Nat.bit b n)
[PROOFSTEP]
rw [bit_val, Nat.bit_val]
[GOAL]
b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + bif b then 1 else 0)
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (2 * ↑n + bif false then 1 else 0) = ↑(2 * n + bif false then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (2 * ↑n + bif true then 1 else 0) = ↑(2 * n + bif true then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℕ
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]
[PROOFSTEP]
rw [bit_val, Nat.bit_val]
[GOAL]
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + bif !b then 1 else 0+1]
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + bif !false then 1 else 0+1]
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + bif !true then 1 else 0+1]
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℤ
⊢ bodd (bit b n) = b
[PROOFSTEP]
rw [bit_val]
[GOAL]
b : Bool
n : ℤ
⊢ bodd (2 * n + bif b then 1 else 0) = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℤ
⊢ bodd (2 * n + bif false then 1 else 0) = false
[PROOFSTEP]
cases bodd n
[GOAL]
case true
n : ℤ
⊢ bodd (2 * n + bif true then 1 else 0) = true
[PROOFSTEP]
cases bodd n
[GOAL]
case false.false
n : ℤ
⊢ bodd (2 * n + bif false then 1 else 0) = false
[PROOFSTEP]
simp
[GOAL]
case false.true
n : ℤ
⊢ bodd (2 * n + bif false then 1 else 0) = false
[PROOFSTEP]
simp
[GOAL]
case true.false
n : ℤ
⊢ bodd (2 * n + bif true then 1 else 0) = true
[PROOFSTEP]
simp
[GOAL]
case true.true
n : ℤ
⊢ bodd (2 * n + bif true then 1 else 0) = true
[PROOFSTEP]
simp
[GOAL]
m n : ℤ
⊢ ¬bodd (bit0 m) = bodd (bit1 n)
[PROOFSTEP]
simp
[GOAL]
m : ℤ
⊢ bit1 m ≠ 0
[PROOFSTEP]
simpa only [bit0_zero] using bit1_ne_bit0 m 0
[GOAL]
b : Bool
n : ℕ
⊢ testBit (bit b ↑n) 0 = b
[PROOFSTEP]
rw [bit_coe_nat]
[GOAL]
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) 0 = b
[PROOFSTEP]
apply Nat.testBit_zero
[GOAL]
b : Bool
n : ℕ
⊢ testBit (bit b -[n+1]) 0 = b
[PROOFSTEP]
rw [bit_negSucc]
[GOAL]
b : Bool
n : ℕ
⊢ testBit -[Nat.bit (!b) n+1] 0 = b
[PROOFSTEP]
dsimp [testBit]
[GOAL]
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) 0) = b
[PROOFSTEP]
rw [Nat.testBit_zero]
[GOAL]
b : Bool
n : ℕ
⊢ (!!b) = b
[PROOFSTEP]
clear testBit_zero
[GOAL]
b : Bool
n : ℕ
⊢ (!!b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (!!false) = false
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (!!true) = true
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b ↑n) (Nat.succ m) = testBit (↑n) m
[PROOFSTEP]
rw [bit_coe_nat]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) (Nat.succ m) = testBit (↑n) m
[PROOFSTEP]
apply Nat.testBit_succ
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b -[n+1]) (Nat.succ m) = testBit -[n+1] m
[PROOFSTEP]
dsimp [testBit]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ (match bit b -[n+1], Nat.succ m with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    !Nat.testBit n m
[PROOFSTEP]
simp only [bit_negSucc]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) (Nat.succ m)) = !Nat.testBit n m
[PROOFSTEP]
cases b
[GOAL]
case false
m n : ℕ
⊢ (!Nat.testBit (Nat.bit (!false) n) (Nat.succ m)) = !Nat.testBit n m
[PROOFSTEP]
simp [Nat.testBit_succ]
[GOAL]
case true
m n : ℕ
⊢ (!Nat.testBit (Nat.bit (!true) n) (Nat.succ m)) = !Nat.testBit n m
[PROOFSTEP]
simp [Nat.testBit_succ]
[GOAL]
⊢ bitwise or = lor
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise or m n = lor m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise or (ofNat m) n = lor (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise or -[m+1] n = lor -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = lor (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = lor (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = lor (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff', negSucc.injEq, Bool.true_or,
  Nat.land']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff', negSucc.injEq, Bool.true_or,
  Nat.land']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff', negSucc.injEq, Bool.true_or,
  Nat.land']
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(x || !y)) m n = Nat.bitwise' (fun a b => a && !b) n m
[PROOFSTEP]
rw [Nat.bitwise'_swap, Function.swap]
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun y x => !(x || !y)) n m = Nat.bitwise' (fun a b => a && !b) n m
case h.h.ofNat.negSucc m n : ℕ ⊢ (!(false || !false)) = false
[PROOFSTEP]
congr
[GOAL]
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun y x => !(x || !y)) = fun a b => a && !b
case h.h.ofNat.negSucc m n : ℕ ⊢ (!(false || !false)) = false
[PROOFSTEP]
funext x y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(y || !x)) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(y || !false)) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(y || !true)) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.false
m n : ℕ
⊢ (!(false || !false)) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.true
m n : ℕ
⊢ (!(true || !false)) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.false
m n : ℕ
⊢ (!(false || !true)) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.true
m n : ℕ
⊢ (!(true || !true)) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ (!(false || !false)) = false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || y)) m n = Nat.bitwise' (fun a b => a && !b) m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x || y)) = fun a b => a && !b
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || y)) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false || y)) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true || y)) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false || false)) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false || true)) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true || false)) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true || true)) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || !y)) m n = Nat.bitwise' and m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_f
m n : ℕ
⊢ (fun x y => !(!x || !y)) = and
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || !y)) = (x && y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false || !y)) = (false && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true || !y)) = (true && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false || !false)) = (false && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false || !true)) = (false && true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true || !false)) = (true && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true || !true)) = (true && true)
[PROOFSTEP]
rfl
[GOAL]
⊢ bitwise and = land
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise and m n = land m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise and (ofNat m) n = land (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise and -[m+1] n = land -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = land (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = land (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = land (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = land (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = land (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = land (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && y) m n) = land -[m+1] (ofNat n)
[PROOFSTEP]
rw [Nat.bitwise'_swap, Function.swap]
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && y) n m) = land -[m+1] (ofNat n)
case h.h.negSucc.ofNat m n : ℕ ⊢ (!false && false) = false
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && y) = fun a b => a && !b
case h.h.negSucc.ofNat m n : ℕ ⊢ (!false && false) = false
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!y && false) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!y && true) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (!false && false) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (!true && false) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (!false && true) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (!true && true) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise' (fun x y => !(!x && !y)) m n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false && !y)) = (false || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true && !y)) = (true || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false && !false)) = (false || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false && !true)) = (false || true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true && !false)) = (true || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true && !true)) = (true || true)
[PROOFSTEP]
rfl
[GOAL]
⊢ (bitwise fun a b => a && !b) = ldiff'
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise (fun a b => a && !b) m n = ldiff' m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) n = ldiff' (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] n = ldiff' -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) (ofNat n) = ldiff' (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) (ofNat n) = ldiff' (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) (ofNat n) = ldiff' (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor']
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => x && !!y) m n) = ↑(Nat.bitwise' and m n)
[PROOFSTEP]
congr
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => x && !!y) = and
[PROOFSTEP]
funext x y
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (x && !!y) = (x && y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (false && !!y) = (false && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (true && !!y) = (true && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (false && !!false) = (false && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (false && !!true) = (false && true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (true && !!false) = (true && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (true && !!true) = (true && true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x && !y)) m n = Nat.bitwise' or m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false && !y)) = (false || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true && !y)) = (true || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false && !false)) = (false || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false && !true)) = (false || true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true && !false)) = (true || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true && !true)) = (true || true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && !!y) m n) = ↑(Nat.bitwise' (fun a b => a && !b) n m)
[PROOFSTEP]
rw [Nat.bitwise'_swap, Function.swap]
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && !!y) n m) = ↑(Nat.bitwise' (fun a b => a && !b) n m)
case h.h.negSucc.negSucc m n : ℕ ⊢ (!false && !!false) = false
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && !!y) = fun a b => a && !b
case h.h.negSucc.negSucc m n : ℕ ⊢ (!false && !!false) = false
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && !!x) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!y && !!false) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!y && !!true) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (!false && !!false) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (!true && !!false) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (!false && !!true) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (!true && !!true) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ (!false && !!false) = false
[PROOFSTEP]
rfl
[GOAL]
⊢ bitwise xor = lxor'
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise xor m n = lxor' m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise xor (ofNat m) n = lxor' (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise xor -[m+1] n = lxor' -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = lxor' (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = lxor' (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = lxor' (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.false_xor, Bool.true_xor, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor', lxor',
  Nat.lxor']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.false_xor, Bool.true_xor, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor', lxor',
  Nat.lxor']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.false_xor, Bool.true_xor, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor', lxor',
  Nat.lxor']
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor x !y) m n = Nat.bitwise' xor m n
[PROOFSTEP]
congr
[GOAL]
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun x y => !xor x !y) = xor
[PROOFSTEP]
funext x y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor x !y) = xor x y
[PROOFSTEP]
cases x
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!xor false !y) = xor false y
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!xor true !y) = xor true y
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.false
m n : ℕ
⊢ (!xor false !false) = xor false false
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.true
m n : ℕ
⊢ (!xor false !true) = xor false true
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.false
m n : ℕ
⊢ (!xor true !false) = xor true false
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.true
m n : ℕ
⊢ (!xor true !true) = xor true true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor (!x) y) m n = Nat.bitwise' xor m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !xor (!x) y) = xor
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor (!x) y) = xor x y
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!xor (!false) y) = xor false y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!xor (!true) y) = xor true y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.false
m n : ℕ
⊢ (!xor (!false) false) = xor false false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.true
m n : ℕ
⊢ (!xor (!false) true) = xor false true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.false
m n : ℕ
⊢ (!xor (!true) false) = xor true false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.true
m n : ℕ
⊢ (!xor (!true) true) = xor true true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => xor (!x) !y) = xor
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (xor (!x) !y) = xor x y
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (xor (!false) !y) = xor false y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (xor (!true) !y) = xor true y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (xor (!false) !false) = xor false false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (xor (!false) !true) = xor false true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (xor (!true) !false) = xor true false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (xor (!true) !true) = xor true true
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b n) = bit (f a b) (bitwise f (ofNat m) n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case negSucc
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (ofNat m) -[n+1])
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))
[PROOFSTEP]
by_cases h : f false false
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false false = true
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false false = true
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))
[PROOFSTEP]
simp [h]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))
[PROOFSTEP]
by_cases h : f false true
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false true = true
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false true = true
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))
[PROOFSTEP]
by_cases h : f true false
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true false = true
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true false = true
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
[PROOFSTEP]
by_cases h : f true true
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true true = true
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true true = true
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ lor (bit a m) (bit b n) = bit (a || b) (lor m n)
[PROOFSTEP]
rw [← bitwise_or, bitwise_bit]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ land (bit a m) (bit b n) = bit (a && b) (land m n)
[PROOFSTEP]
rw [← bitwise_and, bitwise_bit]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ ldiff' (bit a m) (bit b n) = bit (a && !b) (ldiff' m n)
[PROOFSTEP]
rw [← bitwise_diff, bitwise_bit]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ lxor' (bit a m) (bit b n) = bit (xor a b) (lxor' m n)
[PROOFSTEP]
rw [← bitwise_xor, bitwise_bit]
[GOAL]
b : Bool
n : ℕ
⊢ lnot (bit b ↑n) = bit (!b) (lnot ↑n)
[PROOFSTEP]
simp [lnot]
[GOAL]
b : Bool
n : ℕ
⊢ lnot (bit b -[n+1]) = bit (!b) (lnot -[n+1])
[PROOFSTEP]
simp [lnot]
[GOAL]
f : Bool → Bool → Bool
m n : ℤ
k : ℕ
⊢ testBit (bitwise f m n) k = f (testBit m k) (testBit n k)
[PROOFSTEP]
cases m
[GOAL]
case ofNat
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ testBit (bitwise f (ofNat a✝) n) k = f (testBit (ofNat a✝) k) (testBit n k)
[PROOFSTEP]
cases n
[GOAL]
case negSucc
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ testBit (bitwise f -[a✝+1] n) k = f (testBit -[a✝+1] k) (testBit n k)
[PROOFSTEP]
cases n
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f (ofNat a✝¹) (ofNat a✝)) k = f (testBit (ofNat a✝¹) k) (testBit (ofNat a✝) k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f (ofNat a✝¹) -[a✝+1]) k = f (testBit (ofNat a✝¹) k) (testBit -[a✝+1] k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f -[a✝¹+1] (ofNat a✝)) k = f (testBit -[a✝¹+1] k) (testBit (ofNat a✝) k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f -[a✝¹+1] -[a✝+1]) k = f (testBit -[a✝¹+1] k) (testBit -[a✝+1] k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match bif f false false then -[Nat.bitwise' (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise' f a✝¹ a✝), k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
by_cases h : f false false
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false false = true
⊢ (match bif f false false then -[Nat.bitwise' (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise' f a✝¹ a✝), k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false false = true
⊢ (match bif f false false then -[Nat.bitwise' (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise' f a✝¹ a✝), k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f false !false then -[Nat.bitwise' (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
by_cases h : f false true
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise' (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise' (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) false then -[Nat.bitwise' (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
by_cases h : f true false
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise' (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise' (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise' (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
by_cases h : f true true
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise' (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise' (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (lor m n) k = (testBit m k || testBit n k)
[PROOFSTEP]
rw [← bitwise_or, testBit_bitwise]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (land m n) k = (testBit m k && testBit n k)
[PROOFSTEP]
rw [← bitwise_and, testBit_bitwise]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (ldiff' m n) k = (testBit m k && !testBit n k)
[PROOFSTEP]
rw [← bitwise_diff, testBit_bitwise]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (lxor' m n) k = xor (testBit m k) (testBit n k)
[PROOFSTEP]
rw [← bitwise_xor, testBit_bitwise]
[GOAL]
n k : ℕ
⊢ testBit (lnot ↑n) k = !testBit (↑n) k
[PROOFSTEP]
simp [lnot, testBit]
[GOAL]
n k : ℕ
⊢ testBit (lnot -[n+1]) k = !testBit -[n+1] k
[PROOFSTEP]
simp [lnot, testBit]
[GOAL]
m n : ℤ
⊢ shiftr m (-n) = shiftl m n
[PROOFSTEP]
rw [← shiftl_neg, neg_neg]
[GOAL]
m n : ℕ
⊢ shiftr ↑m ↑n = ↑(Nat.shiftr m n)
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
⊢ shiftr ↑m ↑Nat.zero = ↑(Nat.shiftr m Nat.zero)
[PROOFSTEP]
rfl
[GOAL]
case succ
m n✝ : ℕ
⊢ shiftr ↑m ↑(Nat.succ n✝) = ↑(Nat.shiftr m (Nat.succ n✝))
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ shiftr -[m+1] ↑n = -[Nat.shiftr m n+1]
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
⊢ shiftr -[m+1] ↑Nat.zero = -[Nat.shiftr m Nat.zero+1]
[PROOFSTEP]
rfl
[GOAL]
case succ
m n✝ : ℕ
⊢ shiftr -[m+1] ↑(Nat.succ n✝) = -[Nat.shiftr m (Nat.succ n✝)+1]
[PROOFSTEP]
rfl
[GOAL]
m n k : ℕ
⊢ shiftr (↑m) (↑n + ↑k) = shiftr (shiftr ↑m ↑n) ↑k
[PROOFSTEP]
rw [shiftr_coe_nat, shiftr_coe_nat, ← Int.ofNat_add, shiftr_coe_nat, Nat.shiftr_add]
[GOAL]
m n k : ℕ
⊢ shiftr -[m+1] (↑n + ↑k) = shiftr (shiftr -[m+1] ↑n) ↑k
[PROOFSTEP]
rw [shiftr_negSucc, shiftr_negSucc, ← Int.ofNat_add, shiftr_negSucc, Nat.shiftr_add]
[GOAL]
m n✝ k i n : ℕ
⊢ (fun n k i => shiftl (↑m) i = ↑(Nat.shiftr (Nat.shiftl m n) k)) (n + i) n ↑i
[PROOFSTEP]
dsimp
[GOAL]
m n✝ k i n : ℕ
⊢ ↑(Nat.shiftl m i) = ↑(Nat.shiftr (Nat.shiftl m (n + i)) n)
[PROOFSTEP]
rw [← Nat.shiftl_sub, add_tsub_cancel_left]
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
m n✝ k i n : ℕ
⊢ (fun n k i => shiftl (↑m) i = ↑(Nat.shiftr (Nat.shiftl m n) k)) n (n + i + 1) -[i+1]
[PROOFSTEP]
dsimp
[GOAL]
m n✝ k i n : ℕ
⊢ shiftl ↑m -[i+1] = ↑(Nat.shiftr (Nat.shiftl m n) (n + i + 1))
[PROOFSTEP]
rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl_sub, tsub_self]
[GOAL]
m n✝ k i n : ℕ
⊢ shiftl ↑m -[i+1] = ↑(Nat.shiftr (Nat.shiftl m 0) (i + 1))
[PROOFSTEP]
rfl
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n
[PROOFSTEP]
rfl
[GOAL]
m n✝ k i n : ℕ
⊢ Nat.shiftl' true m i = Nat.shiftr (Nat.shiftl' true m (n + i)) n
[PROOFSTEP]
rw [← Nat.shiftl'_sub, add_tsub_cancel_left]
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
m n✝ k i n : ℕ
⊢ Nat.shiftr m (Nat.succ i) = Nat.shiftr (Nat.shiftl' true m n) (n + i + 1)
[PROOFSTEP]
rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl'_sub, tsub_self]
[GOAL]
m n✝ k i n : ℕ
⊢ Nat.shiftr m (Nat.succ i) = Nat.shiftr (Nat.shiftl' true m 0) (i + 1)
[PROOFSTEP]
rfl
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ shiftr ↑m ↑n = ↑m / ↑(2 ^ n)
[PROOFSTEP]
rw [shiftr_coe_nat, Nat.shiftr_eq_div_pow _ _]
[GOAL]
m n : ℕ
⊢ ↑(m / 2 ^ n) = ↑m / ↑(2 ^ n)
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
⊢ shiftr -[m+1] ↑n = -[m+1] / ↑(2 ^ n)
[PROOFSTEP]
rw [shiftr_negSucc, negSucc_ediv, Nat.shiftr_eq_div_pow]
[GOAL]
m n : ℕ
⊢ -[m / 2 ^ n+1] = -(div ↑m ↑(2 ^ n) + 1)
case H m n : ℕ ⊢ 0 < ↑(2 ^ n)
[PROOFSTEP]
rfl
[GOAL]
case H
m n : ℕ
⊢ 0 < ↑(2 ^ n)
[PROOFSTEP]
exact ofNat_lt_ofNat_of_lt (pow_pos (by decide) _)
[GOAL]
m n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide