[GOAL]
m : ℕ
xs : Bitvec m
b : Bool
⊢ Bitvec.toNat (xs++ₜb ::ᵥ Vector.nil) = Bitvec.toNat xs * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)
[PROOFSTEP]
cases' xs with xs P
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
P : List.length xs = m
⊢ Bitvec.toNat ({ val := xs, property := P }++ₜb ::ᵥ Vector.nil) =
    Bitvec.toNat { val := xs, property := P } * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)
[PROOFSTEP]
simp [bitsToNat_toList]
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
P : List.length xs = m
⊢ bitsToNat (xs ++ [b]) = bitsToNat [b] + bitsToNat xs * 2
[PROOFSTEP]
clear P
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ bitsToNat (xs ++ [b]) = bitsToNat [b] + bitsToNat xs * 2
[PROOFSTEP]
unfold bitsToNat
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ List.foldl addLsb 0 (xs ++ [b]) = List.foldl addLsb 0 [b] + List.foldl addLsb 0 xs * 2
[PROOFSTEP]
rw [List.foldl, List.foldl]
  -- generalize the accumulator of foldl
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ List.foldl addLsb 0 (xs ++ [b]) = addLsb 0 b + List.foldl addLsb 0 xs * 2
[PROOFSTEP]
generalize h : 0 = x
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb x b + List.foldl addLsb x xs * 2
[PROOFSTEP]
conv in addLsb x b => rw [← h]
[GOAL]
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
| addLsb x b
[PROOFSTEP]
rw [← h]
[GOAL]
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
| addLsb x b
[PROOFSTEP]
rw [← h]
[GOAL]
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
| addLsb x b
[PROOFSTEP]
rw [← h]
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb 0 b + List.foldl addLsb x xs * 2
[PROOFSTEP]
clear h
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb 0 b + List.foldl addLsb x xs * 2
[PROOFSTEP]
simp
[GOAL]
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
⊢ addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
[PROOFSTEP]
induction' xs with x xs xs_ih generalizing x
[GOAL]
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ addLsb (List.foldl addLsb x []) b = addLsb 0 b + List.foldl addLsb x [] * 2
[PROOFSTEP]
simp
[GOAL]
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ addLsb x b = addLsb 0 b + x * 2
[PROOFSTEP]
unfold addLsb
[GOAL]
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ (x + x + bif b then 1 else 0) = (0 + 0 + bif b then 1 else 0) + x * 2
[PROOFSTEP]
simp [Nat.mul_succ]
[GOAL]
case mk.cons
m : ℕ
b : Bool
x✝¹ : ℕ
x✝ : Bool
xs : List Bool
xs_ih : ∀ (x : ℕ), addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
x : ℕ
⊢ addLsb (List.foldl addLsb x (x✝ :: xs)) b = addLsb 0 b + List.foldl addLsb x (x✝ :: xs) * 2
[PROOFSTEP]
simp
[GOAL]
case mk.cons
m : ℕ
b : Bool
x✝¹ : ℕ
x✝ : Bool
xs : List Bool
xs_ih : ∀ (x : ℕ), addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
x : ℕ
⊢ addLsb (List.foldl addLsb (addLsb x x✝) xs) b = addLsb 0 b + List.foldl addLsb (addLsb x x✝) xs * 2
[PROOFSTEP]
apply xs_ih
[GOAL]
n : ℕ
⊢ Bitvec.toNat (decide (n % 2 = 1) ::ᵥ Vector.nil) = n % 2
[PROOFSTEP]
simp [bitsToNat_toList]
[GOAL]
n : ℕ
⊢ bitsToNat [decide (n % 2 = 1)] = n % 2
[PROOFSTEP]
unfold bitsToNat addLsb List.foldl
[GOAL]
n : ℕ
⊢ List.foldl (fun r b => r + r + bif b then 1 else 0) (0 + 0 + bif decide (n % 2 = 1) then 1 else 0) [] = n % 2
[PROOFSTEP]
simp [Nat.cond_decide_mod_two, -Bool.cond_decide]
[GOAL]
k n : ℕ
⊢ Bitvec.toNat (Bitvec.ofNat k n) = n % 2 ^ k
[PROOFSTEP]
induction' k with k ih generalizing n
[GOAL]
case zero
n✝ n : ℕ
⊢ Bitvec.toNat (Bitvec.ofNat zero n) = n % 2 ^ zero
[PROOFSTEP]
simp [Nat.mod_one]
[GOAL]
case zero
n✝ n : ℕ
⊢ Bitvec.toNat (Bitvec.ofNat 0 n) = 0
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ k : ℕ
ih : ∀ {n : ℕ}, Bitvec.toNat (Bitvec.ofNat k n) = n % 2 ^ k
n : ℕ
⊢ Bitvec.toNat (Bitvec.ofNat (succ k) n) = n % 2 ^ succ k
[PROOFSTEP]
rw [ofNat_succ, toNat_append, ih, bits_toNat_decide, mod_pow_succ, Nat.mul_comm]
[GOAL]
n : ℕ
i : Fin (2 ^ n)
⊢ Bitvec.toNat (ofFin i) = ↑i
[PROOFSTEP]
rw [ofFin, toNat_ofNat, Nat.mod_eq_of_lt]
[GOAL]
n : ℕ
i : Fin (2 ^ n)
⊢ ↑i < 2 ^ n
[PROOFSTEP]
apply i.is_lt
[GOAL]
x : ℕ
b : Bool
⊢ addLsb x b = 2 * x + bif b then 1 else 0
[PROOFSTEP]
simp [addLsb, two_mul]
[GOAL]
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v = List.foldr (flip addLsb) 0 (List.reverse (Vector.toList v))
[PROOFSTEP]
rw [List.foldr_reverse]
[GOAL]
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v = List.foldl (fun x y => flip addLsb y x) 0 (Vector.toList v)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v < 2 ^ n
[PROOFSTEP]
suffices : v.toNat + 1 ≤ 2 ^ n
[GOAL]
n : ℕ
v : Bitvec n
this : Bitvec.toNat v + 1 ≤ 2 ^ n
⊢ Bitvec.toNat v < 2 ^ n
case this n : ℕ v : Bitvec n ⊢ Bitvec.toNat v + 1 ≤ 2 ^ n
[PROOFSTEP]
simpa
[GOAL]
case this
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v + 1 ≤ 2 ^ n
[PROOFSTEP]
rw [toNat_eq_foldr_reverse]
[GOAL]
case this
n : ℕ
v : Bitvec n
⊢ List.foldr (flip addLsb) 0 (List.reverse (Vector.toList v)) + 1 ≤ 2 ^ n
[PROOFSTEP]
cases' v with xs h
[GOAL]
case this.mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ List.foldr (flip addLsb) 0 (List.reverse (Vector.toList { val := xs, property := h })) + 1 ≤ 2 ^ n
[PROOFSTEP]
dsimp [Bitvec.toNat, bitsToNat]
[GOAL]
case this.mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ List.foldr (flip addLsb) 0 (List.reverse xs) + 1 ≤ 2 ^ n
[PROOFSTEP]
rw [← List.length_reverse] at h
[GOAL]
case this.mk
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ List.foldr (flip addLsb) 0 (List.reverse xs) + 1 ≤ 2 ^ n
[PROOFSTEP]
generalize xs.reverse = ys at h
[GOAL]
case this.mk
n : ℕ
xs ys : List Bool
h : List.length ys = n
⊢ List.foldr (flip addLsb) 0 ys + 1 ≤ 2 ^ n
[PROOFSTEP]
induction' ys with head tail ih generalizing n
[GOAL]
case this.mk.nil
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
n : ℕ
h : List.length [] = n
⊢ List.foldr (flip addLsb) 0 [] + 1 ≤ 2 ^ n
[PROOFSTEP]
simp [← h]
[GOAL]
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ List.foldr (flip addLsb) 0 (head :: tail) + 1 ≤ 2 ^ n
[PROOFSTEP]
simp only [← h, pow_add, flip, List.length, List.foldr, pow_one]
[GOAL]
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ addLsb (List.foldr (fun b a => addLsb a b) 0 tail) head + 1 ≤ 2 ^ List.length tail * 2
[PROOFSTEP]
rw [addLsb_eq_twice_add_one]
[GOAL]
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (2 * List.foldr (fun b a => addLsb a b) 0 tail + bif head then 1 else 0) + 1 ≤ 2 ^ List.length tail * 2
[PROOFSTEP]
trans
  2 * List.foldr (fun (x : Bool) (y : ℕ) => addLsb y x) 0 tail +
    2 *
      1
        -- Porting note: removed `ac_mono`, `mono` calls
[GOAL]
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (2 * List.foldr (fun b a => addLsb a b) 0 tail + bif head then 1 else 0) + 1 ≤
    2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1
[PROOFSTEP]
rw [add_assoc]
[GOAL]
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * List.foldr (fun b a => addLsb a b) 0 tail + ((bif head then 1 else 0) + 1) ≤
    2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1
[PROOFSTEP]
apply Nat.add_le_add_left
[GOAL]
case h
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (bif head then 1 else 0) + 1 ≤ 2 * 1
[PROOFSTEP]
cases head
[GOAL]
case h.false
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (false :: tail) = n
⊢ (bif false then 1 else 0) + 1 ≤ 2 * 1
[PROOFSTEP]
simp only
[GOAL]
case h.true
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (true :: tail) = n
⊢ (bif true then 1 else 0) + 1 ≤ 2 * 1
[PROOFSTEP]
simp only
[GOAL]
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1 ≤ 2 ^ List.length tail * 2
[PROOFSTEP]
rw [← left_distrib]
[GOAL]
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * (List.foldr (fun x y => addLsb y x) 0 tail + 1) ≤ 2 ^ List.length tail * 2
[PROOFSTEP]
rw [mul_comm _ 2]
[GOAL]
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * (List.foldr (fun x y => addLsb y x) 0 tail + 1) ≤ 2 * 2 ^ List.length tail
[PROOFSTEP]
apply Nat.mul_le_mul_left
[GOAL]
case h
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ List.foldr (fun x y => addLsb y x) 0 tail + 1 ≤ 2 ^ List.length tail
[PROOFSTEP]
exact ih rfl
[GOAL]
x : ℕ
b : Bool
⊢ addLsb x b / 2 = x
[PROOFSTEP]
cases b
[GOAL]
case false
x : ℕ
⊢ addLsb x false / 2 = x
[PROOFSTEP]
simp only [Nat.add_mul_div_left, addLsb, ← two_mul, add_comm, Nat.succ_pos', Nat.mul_div_right, gt_iff_lt, zero_add,
  cond]
[GOAL]
case true
x : ℕ
⊢ addLsb x true / 2 = x
[PROOFSTEP]
simp only [Nat.add_mul_div_left, addLsb, ← two_mul, add_comm, Nat.succ_pos', Nat.mul_div_right, gt_iff_lt, zero_add,
  cond]
[GOAL]
case true
x : ℕ
⊢ x + 1 / 2 = x
[PROOFSTEP]
norm_num
[GOAL]
x : ℕ
b : Bool
⊢ decide (addLsb x b % 2 = 1) = b
[PROOFSTEP]
cases b
[GOAL]
case false
x : ℕ
⊢ decide (addLsb x false % 2 = 1) = false
[PROOFSTEP]
simp only [Bool.decide_iff, Nat.add_mul_mod_self_left, addLsb, ← two_mul, add_comm, Bool.decide_False,
  Nat.mul_mod_right, zero_add, cond, zero_ne_one]
[GOAL]
case true
x : ℕ
⊢ decide (addLsb x true % 2 = 1) = true
[PROOFSTEP]
simp only [Bool.decide_iff, Nat.add_mul_mod_self_left, addLsb, ← two_mul, add_comm, Bool.decide_False,
  Nat.mul_mod_right, zero_add, cond, zero_ne_one]
[GOAL]
n : ℕ
v : Bitvec n
⊢ Bitvec.ofNat n (Bitvec.toNat v) = v
[PROOFSTEP]
cases' v with xs h
[GOAL]
case mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h }) = { val := xs, property := h }
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ ↑(Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h })) = ↑{ val := xs, property := h }
[PROOFSTEP]
change Vector.toList _ = xs
[GOAL]
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Vector.toList (Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h })) = xs
[PROOFSTEP]
dsimp [Bitvec.toNat, bitsToNat]
[GOAL]
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldl addLsb 0 xs)) = xs
[PROOFSTEP]
rw [← List.length_reverse] at h
[GOAL]
case mk.a
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldl addLsb 0 xs)) = xs
[PROOFSTEP]
rw [← List.reverse_reverse xs, List.foldl_reverse]
[GOAL]
case mk.a
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (List.reverse xs))) =
    List.reverse (List.reverse xs)
[PROOFSTEP]
generalize xs.reverse = ys at h ⊢
[GOAL]
case mk.a
n : ℕ
xs ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys)) = List.reverse ys
[PROOFSTEP]
clear xs
[GOAL]
case mk.a
n : ℕ
ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys)) = List.reverse ys
[PROOFSTEP]
induction' ys with ys_head ys_tail ys_ih generalizing n
[GOAL]
case mk.a.nil
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
n : ℕ
h : List.length [] = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 [])) = List.reverse []
[PROOFSTEP]
cases h
[GOAL]
case mk.a.nil.refl
n : ℕ
ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat (List.length []) (List.foldr (fun x y => addLsb y x) 0 [])) = List.reverse []
[PROOFSTEP]
simp [Bitvec.ofNat]
[GOAL]
case mk.a.cons
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
n : ℕ
h : List.length (ys_head :: ys_tail) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
[PROOFSTEP]
simp only [← Nat.succ_eq_add_one, List.length] at h
[GOAL]
case mk.a.cons
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
n : ℕ
h : succ (List.length ys_tail) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
[PROOFSTEP]
subst n
[GOAL]
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList
      (Bitvec.ofNat (succ (List.length ys_tail)) (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
[PROOFSTEP]
simp only [Bitvec.ofNat, Vector.toList_cons, Vector.toList_nil, List.reverse_cons, Vector.toList_append, List.foldr]
[GOAL]
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList
        (Bitvec.ofNat (List.length ys_tail) (addLsb (List.foldr (fun x y => addLsb y x) 0 ys_tail) ys_head / 2)) ++
      [decide (addLsb (List.foldr (fun x y => addLsb y x) 0 ys_tail) ys_head % 2 = 1)] =
    List.reverse ys_tail ++ [ys_head]
[PROOFSTEP]
erw [addLsb_div_two, decide_addLsb_mod_two]
[GOAL]
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList (Bitvec.ofNat (List.length ys_tail) (List.foldr (fun x y => addLsb y x) 0 ys_tail)) ++ [ys_head] =
    List.reverse ys_tail ++ [ys_head]
[PROOFSTEP]
congr
[GOAL]
case mk.a.cons.e_a
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList (Bitvec.ofNat (List.length ys_tail) (List.foldr (fun x y => addLsb y x) 0 ys_tail)) =
    List.reverse ys_tail
[PROOFSTEP]
apply ys_ih
[GOAL]
case mk.a.cons.e_a.h
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ List.length ys_tail = List.length ys_tail
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
v : Bitvec n
⊢ ↑(toFin v) = Bitvec.toNat v
[PROOFSTEP]
rw [toFin, Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt]
[GOAL]
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v < 2 ^ n
[PROOFSTEP]
apply toNat_lt
[GOAL]
n : ℕ
v₀ v₁ : Bitvec n
h : v₀ ≤ v₁
⊢ ↑(toFin v₀) ≤ ↑(toFin v₁)
[PROOFSTEP]
rw [toFin_val, toFin_val]
[GOAL]
n : ℕ
v₀ v₁ : Bitvec n
h : v₀ ≤ v₁
⊢ Bitvec.toNat v₀ ≤ Bitvec.toNat v₁
[PROOFSTEP]
exact h
[GOAL]
n : ℕ
i j : Fin (2 ^ n)
h : i ≤ j
⊢ Bitvec.toNat (Bitvec.ofNat n ↑i) ≤ Bitvec.toNat (Bitvec.ofNat n ↑j)
[PROOFSTEP]
simp only [toNat_ofNat, Nat.mod_eq_of_lt, Fin.is_lt]
[GOAL]
n : ℕ
i j : Fin (2 ^ n)
h : i ≤ j
⊢ ↑i ≤ ↑j
[PROOFSTEP]
exact h
[GOAL]
n : ℕ
i : Fin (2 ^ n)
⊢ ↑(toFin (ofFin i)) = ↑i
[PROOFSTEP]
simp [toFin_val, ofFin, toNat_ofNat, Nat.mod_eq_of_lt, i.is_lt]
[GOAL]
n : ℕ
v : Bitvec n
⊢ ofFin (toFin v) = v
[PROOFSTEP]
dsimp [ofFin]
[GOAL]
n : ℕ
v : Bitvec n
⊢ Bitvec.ofNat n ↑(toFin v) = v
[PROOFSTEP]
rw [toFin_val, ofNat_toNat]


[GOAL]
n : ℕ
⊢ range (succ n) = n ::ₘ range n
[PROOFSTEP]
rw [range, List.range_succ, ← coe_add, add_comm]
[GOAL]
n : ℕ
⊢ ↑[n] + ↑(List.range n) = n ::ₘ range n
[PROOFSTEP]
rfl
[GOAL]
a : ℕ
m : Multiset ℕ
⊢ Disjoint (range a) (map (fun x => a + x) m)
[PROOFSTEP]
intro x hxa hxb
[GOAL]
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x => a + x) m
⊢ False
[PROOFSTEP]
rw [range, mem_coe, List.mem_range] at hxa
[GOAL]
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x => a + x) m
⊢ False
[PROOFSTEP]
obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
[GOAL]
case intro.intro
a : ℕ
m : Multiset ℕ
c : ℕ
left✝ : c ∈ m
hxa : a + c < a
hxb : a + c ∈ map (fun x => a + x) m
⊢ False
[PROOFSTEP]
exact (self_le_add_right _ _).not_lt hxa
[GOAL]
a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x => a + x) (range b)
[PROOFSTEP]
rw [range_add, add_eq_union_iff_disjoint]
[GOAL]
a b : ℕ
⊢ Disjoint (range a) (map (fun x => a + x) (range b))
[PROOFSTEP]
apply range_disjoint_map_add


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x y : ToType m
⊢ x.fst = y.fst ↔ x.fst = y.fst
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
y : ToType m
fst✝ : α
snd✝ : Fin (count fst✝ m)
⊢ { fst := fst✝, snd := snd✝ }.fst = y.fst ↔ { fst := fst✝, snd := snd✝ }.fst = y.fst
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
fst✝¹ : α
snd✝¹ : Fin (count fst✝¹ m)
fst✝ : α
snd✝ : Fin (count fst✝ m)
⊢ { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst ↔
    { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ ∀ (x : α × ℕ),
    (x ∈
        Finset.biUnion (Multiset.toFinset m) fun x =>
          Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) }
            (Finset.range (Multiset.count x m))) ↔
      x ∈ {p | p.snd < Multiset.count p.fst m}
[PROOFSTEP]
rintro ⟨x, i⟩
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ ((x, i) ∈
      Finset.biUnion (Multiset.toFinset m) fun x =>
        Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) }
          (Finset.range (Multiset.count x m))) ↔
    (x, i) ∈ {p | p.snd < Multiset.count p.fst m}
[PROOFSTEP]
simp only [Finset.mem_biUnion, Multiset.mem_toFinset, Finset.mem_map, Finset.mem_range, Function.Embedding.coeFn_mk,
  Prod.mk.inj_iff, Set.mem_setOf_eq]
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ (∃ a, a ∈ m ∧ ∃ a_1, a_1 < Multiset.count a m ∧ a = x ∧ a_1 = i) ↔ i < Multiset.count x m
[PROOFSTEP]
simp only [← and_assoc, exists_eq_right, and_iff_right_iff_imp]
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ i < Multiset.count x m → x ∈ m
[PROOFSTEP]
exact fun h ↦ Multiset.count_pos.mp (pos_of_gt h)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
⊢ toEnumFinset m₁ ⊆ toEnumFinset m₂
[PROOFSTEP]
intro p
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ toEnumFinset m₁ → p ∈ toEnumFinset m₂
[PROOFSTEP]
simp only [Multiset.mem_toEnumFinset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.snd < count p.fst m₁ → p.snd < count p.fst m₂
[PROOFSTEP]
exact gt_of_ge_of_gt (Multiset.le_iff_count.mp h p.1)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
⊢ toEnumFinset m₁ ⊆ toEnumFinset m₂ ↔ m₁ ≤ m₂
[PROOFSTEP]
refine' ⟨fun h ↦ _, Multiset.toEnumFinset_mono⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ m₁ ≤ m₂
[PROOFSTEP]
rw [Multiset.le_iff_count]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ ∀ (a : α), count a m₁ ≤ count a m₂
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
⊢ count x m₁ ≤ count x m₂
[PROOFSTEP]
by_cases hx : x ∈ m₁
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ count x m₁ ≤ count x m₂
[PROOFSTEP]
apply Nat.le_of_pred_lt
[GOAL]
case pos.a
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ Nat.pred (count x m₁) < count x m₂
[PROOFSTEP]
have : (x, m₁.count x - 1) ∈ m₁.toEnumFinset :=
  by
  rw [Multiset.mem_toEnumFinset]
  exact Nat.pred_lt (ne_of_gt (Multiset.count_pos.mpr hx))
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ (x, count x m₁ - 1) ∈ toEnumFinset m₁
[PROOFSTEP]
rw [Multiset.mem_toEnumFinset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ (x, count x m₁ - 1).snd < count (x, count x m₁ - 1).fst m₁
[PROOFSTEP]
exact Nat.pred_lt (ne_of_gt (Multiset.count_pos.mpr hx))
[GOAL]
case pos.a
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
this : (x, count x m₁ - 1) ∈ toEnumFinset m₁
⊢ Nat.pred (count x m₁) < count x m₂
[PROOFSTEP]
simpa only [Multiset.mem_toEnumFinset] using h this
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : ¬x ∈ m₁
⊢ count x m₁ ≤ count x m₂
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.Injective fun x => (x.fst, ↑x.snd)
[PROOFSTEP]
intro ⟨x, i, hi⟩ ⟨y, j, hj⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
hi : i < count x m
y : α
j : ℕ
hj : j < count y m
⊢ (fun x => (x.fst, ↑x.snd)) { fst := x, snd := { val := i, isLt := hi } } =
      (fun x => (x.fst, ↑x.snd)) { fst := y, snd := { val := j, isLt := hj } } →
    { fst := x, snd := { val := i, isLt := hi } } = { fst := y, snd := { val := j, isLt := hj } }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refl
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
hi hj : i < count x m
⊢ { fst := x, snd := { val := i, isLt := hi } } = { fst := x, snd := { val := i, isLt := hj } }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : ToType m
⊢ ↑(coeEmbedding m) x ∈ toEnumFinset m
[PROOFSTEP]
rw [Multiset.mem_toEnumFinset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : ToType m
⊢ (↑(coeEmbedding m) x).snd < count (↑(coeEmbedding m) x).fst m
[PROOFSTEP]
exact x.2.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : { x // x ∈ toEnumFinset m }
⊢ (↑x).snd < count (↑x).fst m
[PROOFSTEP]
rw [← Multiset.mem_toEnumFinset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : { x // x ∈ toEnumFinset m }
⊢ ↑x ∈ toEnumFinset m
[PROOFSTEP]
exact x.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.LeftInverse
    (fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } }) fun x =>
    { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) }
[PROOFSTEP]
rintro ⟨x, i, h⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
h : i < count x m
⊢ (fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } })
      ((fun x => { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) })
        { fst := x, snd := { val := i, isLt := h } }) =
    { fst := x, snd := { val := i, isLt := h } }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.RightInverse
    (fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } }) fun x =>
    { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) }
[PROOFSTEP]
rintro ⟨⟨x, i⟩, h⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
h : (x, i) ∈ toEnumFinset m
⊢ (fun x => { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) })
      ((fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } })
        { val := (x, i), property := h }) =
    { val := (x, i), property := h }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.Embedding.trans (Equiv.toEmbedding (coeEquiv m)) (Function.Embedding.subtype fun x => x ∈ toEnumFinset m) =
    coeEmbedding m
[PROOFSTEP]
ext
[GOAL]
case h.h₁
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x✝ : ToType m
⊢ (↑(Function.Embedding.trans (Equiv.toEmbedding (coeEquiv m)) (Function.Embedding.subtype fun x => x ∈ toEnumFinset m))
        x✝).fst =
    (↑(coeEmbedding m) x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x✝ : ToType m
⊢ (↑(Function.Embedding.trans (Equiv.toEmbedding (coeEquiv m)) (Function.Embedding.subtype fun x => x ∈ toEnumFinset m))
        x✝).snd =
    (↑(coeEmbedding m) x✝).snd
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.map (coeEmbedding m) Finset.univ = toEnumFinset m
[PROOFSTEP]
ext ⟨x, i⟩
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ Finset.map (coeEmbedding m) Finset.univ ↔ (x, i) ∈ toEnumFinset m
[PROOFSTEP]
simp only [Fin.exists_iff, Finset.mem_map, Finset.mem_univ, Multiset.coeEmbedding_apply, Prod.mk.inj_iff,
  exists_true_left, Multiset.exists_coe, Multiset.coe_mk, Fin.val_mk, exists_prop, exists_eq_right_right,
  exists_eq_right, Multiset.mem_toEnumFinset, iff_self_iff, true_and_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
⊢ Finset.filter (fun p => x = p.fst) (toEnumFinset m) =
    Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) } (Finset.range (count x m))
[PROOFSTEP]
ext ⟨y, i⟩
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x y : α
i : ℕ
⊢ (y, i) ∈ Finset.filter (fun p => x = p.fst) (toEnumFinset m) ↔
    (y, i) ∈ Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) } (Finset.range (count x m))
[PROOFSTEP]
simp only [eq_comm, Finset.mem_filter, Multiset.mem_toEnumFinset, Finset.mem_map, Finset.mem_range,
  Function.Embedding.coeFn_mk, Prod.mk.inj_iff, exists_prop, exists_eq_right_right', and_congr_left_iff]
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x y : α
i : ℕ
⊢ x = y → (i < count y m ↔ i < count x m)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
⊢ i < count x m ↔ i < count x m
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map Prod.fst (toEnumFinset m).val = m
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
⊢ count x (map Prod.fst (toEnumFinset m).val) = count x m
[PROOFSTEP]
simp only [Multiset.count_map, ← Finset.filter_val, Multiset.toEnumFinset_filter_eq, Finset.map_val, Finset.range_val,
  Multiset.card_map, Multiset.card_range]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.image Prod.fst (toEnumFinset m) = toFinset m
[PROOFSTEP]
rw [Finset.image, Multiset.map_toEnumFinset_fst]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map (fun x => x.fst) Finset.univ.val = m
[PROOFSTEP]
have := m.map_toEnumFinset_fst
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (toEnumFinset m).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
[PROOFSTEP]
rw [← m.map_univ_coeEmbedding] at this
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (Finset.map (coeEmbedding m) Finset.univ).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
[PROOFSTEP]
simpa only [Finset.map_val, Multiset.coeEmbedding_apply, Multiset.map_map, Function.comp_apply] using this
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ : Multiset α
β : Type u_2
m : Multiset α
f : α → β
⊢ map (fun x => f x.fst) Finset.univ.val = map f m
[PROOFSTEP]
erw [← Multiset.map_map]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ : Multiset α
β : Type u_2
m : Multiset α
f : α → β
⊢ map f (map (fun x => x.fst) Finset.univ.val) = map f m
[PROOFSTEP]
rw [Multiset.map_univ_coe]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.card (toEnumFinset m) = ↑card m
[PROOFSTEP]
rw [Finset.card, ← Multiset.card_map Prod.fst m.toEnumFinset.val]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ ↑card (map Prod.fst (toEnumFinset m).val) = ↑card m
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map Prod.fst (toEnumFinset m).val = m
[PROOFSTEP]
exact m.map_toEnumFinset_fst
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Fintype.card (ToType m) = ↑card m
[PROOFSTEP]
rw [Fintype.card_congr m.coeEquiv]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Fintype.card { x // x ∈ toEnumFinset m } = ↑card m
[PROOFSTEP]
simp only [Fintype.card_coe, card_toEnumFinset]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ prod m = ∏ x : ToType m, x.fst
[PROOFSTEP]
congr
  -- Porting note: `simp` fails with "maximum recursion depth has been reached"
[GOAL]
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.fst) Finset.univ.val
[PROOFSTEP]
erw [map_univ_coe]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ prod m = ∏ x in toEnumFinset m, x.fst
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.fst) (toEnumFinset m).val
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x in toEnumFinset m, f x.fst x.snd = ∏ x : ToType m, f x.fst ↑x.snd
[PROOFSTEP]
rw [Fintype.prod_equiv m.coeEquiv (fun x ↦ f x x.2) fun x ↦ f x.1.1 x.1.2]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x in toEnumFinset m, f x.fst x.snd = ∏ x : { x // x ∈ toEnumFinset m }, f (↑x).fst (↑x).snd
[PROOFSTEP]
rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : ToType m), f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
x : ToType m
⊢ f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
[PROOFSTEP]
rfl


[GOAL]
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (↑M ⊗[R] ↑N))
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (tensorHom (𝟙 M) (𝟙 N)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (𝟙 (of R (↑M ⊗[R] ↑N)))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
⊢ LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃) = LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
⊢ ∀ (x : X₁) (y : X₂) (z : X₃),
    ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro x y z
[GOAL]
case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
x : X₁
y : X₂
z : X₃
⊢ ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
rfl
  -- Porting note: private so hopeful never used outside this file
  -- #align Module.monoidal_category.associator_naturality_aux ModuleCat.MonoidalCategory.associator_naturality_aux
[GOAL]
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
⊢ LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1) =
    LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)
[PROOFSTEP]
apply TensorProduct.ext_fourfold
[GOAL]
case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
⊢ ∀ (w : W) (x : X) (y : Y) (z : Z),
    ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro w x y z
[GOAL]
case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
w : W
x : X
y : Y
z : Z
⊢ ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
rfl
  -- Porting note: private so hopeful never used outside this file
  -- #align Module.monoidal_category.pentagon_aux Module.monoidal_category.pentagon_aux
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)
[PROOFSTEP]
convert associator_naturality_aux f₁ f₂ f₃ using 1
[GOAL]
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ tensorHom (associator W X Y).hom (𝟙 Z) ≫
      (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
    (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom
[PROOFSTEP]
convert pentagon_aux R W X Y Z using 1
[GOAL]
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1 =
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ∀ (x : ↑M),
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1) x =
      ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1) x
[PROOFSTEP]
intro x
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1) x =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1) x
[PROOFSTEP]
change ((leftUnitor N).hom) ((tensorHom (𝟙 (of R R)) f) ((1 : R) ⊗ₜ[R] x)) = f (((leftUnitor M).hom) (1 ⊗ₜ[R] x))
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(leftUnitor N).hom (↑(tensorHom (𝟙 (of R R)) f) (1 ⊗ₜ[R] x)) = ↑f (↑(leftUnitor M).hom (1 ⊗ₜ[R] x))
[PROOFSTEP]
erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (1, x).fst • ↑f (1, x).snd = ↑f (1 • x)
[PROOFSTEP]
rw [LinearMap.map_smul]
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (1, x).fst • ↑f (1, x).snd = 1 • ↑f x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ∀ (x : ↑M),
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x =
      ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x
[PROOFSTEP]
intro x
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x =
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x) 1 =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x) 1
[PROOFSTEP]
change ((rightUnitor N).hom) ((tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] (1 : R))) = f (((rightUnitor M).hom) (x ⊗ₜ[R] 1))
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(rightUnitor N).hom (↑(tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] 1)) = ↑f (↑(rightUnitor M).hom (x ⊗ₜ[R] 1))
[PROOFSTEP]
erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (x, 1).snd • ↑f (x, 1).fst = ↑f (1 • x)
[PROOFSTEP]
rw [LinearMap.map_smul]
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (x, 1).snd • ↑f (x, 1).fst = 1 • ↑f x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro x y z
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
change R at y
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
change x ⊗ₜ[R] ((leftUnitor N).hom) (y ⊗ₜ[R] z) = ((rightUnitor M).hom) (x ⊗ₜ[R] y) ⊗ₜ[R] z
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] ↑(leftUnitor N).hom (y ⊗ₜ[R] z) = ↑(rightUnitor M).hom (x ⊗ₜ[R] y) ⊗ₜ[R] z
[PROOFSTEP]
erw [TensorProduct.lid_tmul, TensorProduct.rid_tmul]
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] (y • z) = (y • x) ⊗ₜ[R] z
[PROOFSTEP]
exact (TensorProduct.smul_tmul _ _ _).symm
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalPreadditive (ModuleCat R)
[PROOFSTEP]
refine' ⟨_, _, _, _⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X), f ⊗ 0 = 0
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X), f ⊗ 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
⊢ f✝ ⊗ 0 = 0
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ 0)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) 0) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ ⊗ 0) (x ⊗ₜ[R] y) = ↑0 (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply, TensorProduct.tmul_zero]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : Y ⟶ Z), 0 ⊗ f = 0
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : Y ⟶ Z), 0 ⊗ f = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
⊢ 0 ⊗ f✝ = 0
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (0 ⊗ f✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) 0) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(0 ⊗ f✝) (x ⊗ₜ[R] y) = ↑0 (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply, TensorProduct.zero_tmul]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h
[PROOFSTEP]
intros
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
⊢ f✝ ⊗ (g✝ + h✝) = f✝ ⊗ g✝ + f✝ ⊗ h✝
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ (g✝ + h✝))) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ g✝ + f✝ ⊗ h✝)) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ ⊗ (g✝ + h✝)) (x ⊗ₜ[R] y) = ↑(f✝ ⊗ g✝ + f✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑f✝ x ⊗ₜ[R] ↑(g✝ + h✝) y = ↑f✝ x ⊗ₜ[R] ↑g✝ y + ↑(f✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
erw [MonoidalCategory.hom_apply]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑f✝ x ⊗ₜ[R] ↑(g✝ + h✝) y = ↑f✝ x ⊗ₜ[R] ↑g✝ y + ↑f✝ x ⊗ₜ[R] ↑h✝ y
[PROOFSTEP]
rw [LinearMap.add_apply, TensorProduct.tmul_add]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h
[PROOFSTEP]
intros
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ⊗ h✝ = f✝ ⊗ h✝ + g✝ ⊗ h✝
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) ((f✝ + g✝) ⊗ h✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ h✝ + g✝ ⊗ h✝)) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑((f✝ + g✝) ⊗ h✝) (x ⊗ₜ[R] y) = ↑(f✝ ⊗ h✝ + g✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ + g✝) x ⊗ₜ[R] ↑h✝ y = ↑f✝ x ⊗ₜ[R] ↑h✝ y + ↑(g✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
erw [MonoidalCategory.hom_apply]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ + g✝) x ⊗ₜ[R] ↑h✝ y = ↑f✝ x ⊗ₜ[R] ↑h✝ y + ↑g✝ x ⊗ₜ[R] ↑h✝ y
[PROOFSTEP]
rw [LinearMap.add_apply, TensorProduct.add_tmul]
  -- Porting note: simp wasn't firing but rw was, annoying
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (ModuleCat R)
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ⊗ r✝ • g✝ = r✝ • (f✝ ⊗ g✝)
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ r✝ • g✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (r✝ • (f✝ ⊗ g✝))) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ ⊗ r✝ • g✝) (x ⊗ₜ[R] y) = ↑(r✝ • (f✝ ⊗ g✝)) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply, LinearMap.smul_apply,
  TensorProduct.tmul_smul]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : W✝ ⟶ X✝
g✝ : Y✝ ⟶ Z✝
⊢ r✝ • f✝ ⊗ g✝ = r✝ • (f✝ ⊗ g✝)
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : W✝ ⟶ X✝
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (r✝ • f✝ ⊗ g✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (r✝ • (f✝ ⊗ g✝))) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : W✝ ⟶ X✝
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(r✝ • f✝ ⊗ g✝) (x ⊗ₜ[R] y) = ↑(r✝ • (f✝ ⊗ g✝)) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply, LinearMap.smul_apply,
  TensorProduct.smul_tmul, TensorProduct.tmul_smul]


[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b ↔
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b →
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
cases' a with a a
[GOAL]
case mp.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
⊢ c ∈ sumLift₂ f g (inl a) b →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
cases' b with b b
[GOAL]
case mp.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
⊢ c ∈ sumLift₂ f g (inr a) b →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
cases' b with b b
[GOAL]
case mp.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
⊢ c ∈ sumLift₂ f g (inl a) (inl b) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rw [sumLift₂, mem_map]
[GOAL]
case mp.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
⊢ (∃ a_1, a_1 ∈ f a b ∧ ↑Embedding.inl a_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rintro ⟨c, hc, rfl⟩
[GOAL]
case mp.inl.inl.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f a b
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ ↑Embedding.inl c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ ↑Embedding.inl c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩
[GOAL]
case mp.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
⊢ c ∈ sumLift₂ f g (inl a) (inr b) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
refine' fun h ↦ (not_mem_empty _ h).elim
[GOAL]
case mp.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₁
⊢ c ∈ sumLift₂ f g (inr a) (inl b) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
refine' fun h ↦ (not_mem_empty _ h).elim
[GOAL]
case mp.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ c ∈ sumLift₂ f g (inr a) (inr b) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rw [sumLift₂, mem_map]
[GOAL]
case mp.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ (∃ a_1, a_1 ∈ g a b ∧ ↑Embedding.inr a_1 = c) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rintro ⟨c, hc, rfl⟩
[GOAL]
case mp.inr.inr.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ g a b
⊢ (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ ↑Embedding.inr c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ ↑Embedding.inr c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
exact Or.inr ⟨a, b, c, rfl, rfl, rfl, hc⟩
[GOAL]
case mpr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂) →
    c ∈ sumLift₂ f g a b
[PROOFSTEP]
rintro (⟨a, b, c, rfl, rfl, rfl, h⟩ | ⟨a, b, c, rfl, rfl, rfl, h⟩)
[GOAL]
case mpr.inl.intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
h : c ∈ f a b
⊢ inl c ∈ sumLift₂ f g (inl a) (inl b)
[PROOFSTEP]
exact mem_map_of_mem _ h
[GOAL]
case mpr.inr.intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
h : c ∈ g a b
⊢ inr c ∈ sumLift₂ f g (inr a) (inr b)
[PROOFSTEP]
exact mem_map_of_mem _ h
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
[PROOFSTEP]
rw [mem_sumLift₂, or_iff_left]
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ (∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
simp only [inl.injEq, exists_and_left, exists_eq_left']
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rintro ⟨_, _, c₂, _, _, h, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
w✝¹ : α₂
w✝ : β₂
c₂ : γ₂
left✝¹ : a = inr w✝¹
left✝ : b = inr w✝
h : inl c₁ = inr c₂
right✝ : c₂ ∈ g w✝¹ w✝
⊢ False
[PROOFSTEP]
exact inl_ne_inr h
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ inr c₂ ∈ sumLift₂ f g a b ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rw [mem_sumLift₂, or_iff_right]
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ (∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
[PROOFSTEP]
simp only [inr.injEq, exists_and_left, exists_eq_left']
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
[PROOFSTEP]
rintro ⟨_, _, c₂, _, _, h, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂✝ : γ₂
w✝¹ : α₁
w✝ : β₁
c₂ : γ₁
left✝¹ : a = inl w✝¹
left✝ : b = inl w✝
h : inr c₂✝ = inl c₂
right✝ : c₂ ∈ f w✝¹ w✝
⊢ False
[PROOFSTEP]
exact inr_ne_inl h
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ sumLift₂ f g a b = ∅ ↔
    (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h : sumLift₂ f g a b = ∅
⊢ (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
[PROOFSTEP]
constructor
[GOAL]
case refine'_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅
[PROOFSTEP]
rintro a b rfl rfl
[GOAL]
case refine'_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
h : sumLift₂ f g (inl a) (inl b) = ∅
⊢ f a b = ∅
[PROOFSTEP]
exact map_eq_empty.1 h
[GOAL]
case refine'_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
[PROOFSTEP]
rintro a b rfl rfl
[GOAL]
case refine'_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
h : sumLift₂ f g (inr a) (inr b) = ∅
⊢ g a b = ∅
[PROOFSTEP]
exact map_eq_empty.1 h
[GOAL]
case refine'_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g a b = ∅
[PROOFSTEP]
cases a
[GOAL]
case refine'_2.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
val✝ : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝) b = ∅
[PROOFSTEP]
cases b
[GOAL]
case refine'_2.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
val✝ : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝) b = ∅
[PROOFSTEP]
cases b
[GOAL]
case refine'_2.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₁
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inl val✝) = ∅
[PROOFSTEP]
exact map_eq_empty.2 (h.1 _ _ rfl rfl)
[GOAL]
case refine'_2.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₁
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inr val✝) = ∅
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₂
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inl val✝) = ∅
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₂
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inr val✝) = ∅
[PROOFSTEP]
exact map_eq_empty.2 (h.2 _ _ rfl rfl)
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ Finset.Nonempty (sumLift₂ f g a b) ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ Finset.Nonempty (f a₁ b₁)) ∨
      ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ Finset.Nonempty (g a₂ b₂)
[PROOFSTEP]
simp only [nonempty_iff_ne_empty, Ne, sumLift₂_eq_empty, not_and_or, not_forall, not_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Icc Icc a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inl a) (inl b) ↔ inl a ≤ inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inl a) (inl b) ↔ inl a ≤ inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inl a) (inr b) ↔ inl a ≤ inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inl a) (inr b) ↔ inl a ≤ inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inr a) (inl b) ↔ inr a ≤ inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inr a) (inl b) ↔ inr a ≤ inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inr a) (inr b) ↔ inr a ≤ inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inr a) (inr b) ↔ inr a ≤ inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ico Ico a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inl a) (inl b) ↔ inl a ≤ inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inl a) (inl b) ↔ inl a ≤ inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inl a) (inr b) ↔ inl a ≤ inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inl a) (inr b) ↔ inl a ≤ inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inr a) (inl b) ↔ inr a ≤ inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inr a) (inl b) ↔ inr a ≤ inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inr a) (inr b) ↔ inr a ≤ inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inr a) (inr b) ↔ inr a ≤ inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioc Ioc a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inl a) (inl b) ↔ inl a < inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inl a) (inl b) ↔ inl a < inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inl a) (inr b) ↔ inl a < inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inl a) (inr b) ↔ inl a < inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inr a) (inl b) ↔ inr a < inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inr a) (inl b) ↔ inr a < inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inr a) (inr b) ↔ inr a < inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inr a) (inr b) ↔ inr a < inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioo Ioo a b ↔ a < x ∧ x < b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inl a) (inl b) ↔ inl a < inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inl a) (inl b) ↔ inl a < inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inl a) (inr b) ↔ inl a < inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inl a) (inr b) ↔ inl a < inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inr a) (inl b) ↔ inr a < inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inr a) (inl b) ↔ inr a < inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inr a) (inr b) ↔ inr a < inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inr a) (inr b) ↔ inr a < inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
b₁ b₂ : β
a b : α ⊕ β
⊢ Ioo (inl a₁) (inr b₂) = ∅
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
b₁ b₂ : β
a b : α ⊕ β
⊢ Ioo (inr b₁) (inl a₂) = ∅
[PROOFSTEP]
rfl