[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin n → β
⊢ ∏ i : Fin n, f i = List.prod (List.map f (List.finRange n))
[PROOFSTEP]
simp [univ_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin n → β
⊢ List.prod (List.ofFn f) = ∏ i : Fin n, f i
[PROOFSTEP]
rw [List.ofFn_eq_map, prod_univ_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
x : Fin (n + 1)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (succAbove x i)
[PROOFSTEP]
rw [univ_succAbove, prod_cons, Finset.prod_map _ x.succAboveEmb.toEmbedding, RelEmbedding.coe_toEmbedding]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
x : Fin (n + 1)
⊢ f x * ∏ x_1 : Fin n, f (↑(succAboveEmb x) x_1) = f x * ∏ i : Fin n, f (succAbove x i)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
⊢ ∏ i : Fin (n + 1), f i = (∏ i : Fin n, f (castSucc i)) * f (last n)
[PROOFSTEP]
simpa [mul_comm] using prod_univ_succAbove f (last n)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
x : β
f : Fin n → β
⊢ ∏ i : Fin (Nat.succ n), cons x f i = x * ∏ i : Fin n, f i
[PROOFSTEP]
simp_rw [prod_univ_succ, cons_zero, cons_succ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 1 → β
⊢ ∏ i : Fin 1, f i = f 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 2 → β
⊢ ∏ i : Fin 2, f i = f 0 * f 1
[PROOFSTEP]
simp [prod_univ_succ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 3 → β
⊢ ∏ i : Fin 3, f i = f 0 * f 1 * f 2
[PROOFSTEP]
rw [prod_univ_castSucc, prod_univ_two]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 3 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 4 → β
⊢ ∏ i : Fin 4, f i = f 0 * f 1 * f 2 * f 3
[PROOFSTEP]
rw [prod_univ_castSucc, prod_univ_three]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 4 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ ∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4
[PROOFSTEP]
rw [prod_univ_castSucc, prod_univ_four]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 6 → β
⊢ ∏ i : Fin 6, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
[PROOFSTEP]
rw [prod_univ_castSucc, prod_univ_five]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 6 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (last 5) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 7 → β
⊢ ∏ i : Fin 7, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
[PROOFSTEP]
rw [prod_univ_castSucc, prod_univ_six]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 7 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (last 6) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 8 → β
⊢ ∏ i : Fin 8, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
[PROOFSTEP]
rw [prod_univ_castSucc, prod_univ_seven]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
f : Fin 8 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (castSucc 6) *
      f (last 7) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
R : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ ∑ s : Finset (Fin n), a ^ card s * b ^ (n - card s) = (a + b) ^ n
[PROOFSTEP]
simpa using Fintype.sum_pow_mul_eq_add_pow (Fin n) a b
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
x : α
⊢ ∏ _i : Fin n, x = x ^ n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
n : ℕ
x : α
⊢ ∑ _i : Fin n, x = n • x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
v : Fin (Nat.succ n) → M
⊢ ∏ i in Ioi 0, v i = ∏ j : Fin n, v (succ j)
[PROOFSTEP]
rw [Ioi_zero_eq_map, Finset.prod_map, RelEmbedding.coe_toEmbedding, val_succEmbedding]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
i : Fin n
v : Fin (Nat.succ n) → M
⊢ ∏ j in Ioi (succ i), v j = ∏ j in Ioi i, v (succ j)
[PROOFSTEP]
rw [Ioi_succ, Finset.prod_map, RelEmbedding.coe_toEmbedding, val_succEmbedding]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin b → M
h : a = b
⊢ ∏ i : Fin a, f (↑(castIso h) i) = ∏ i : Fin b, f i
[PROOFSTEP]
subst h
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a : ℕ
f : Fin a → M
⊢ ∏ i : Fin a, f (↑(castIso (_ : a = a)) i) = ∏ i : Fin a, f i
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ i : Fin (a + b), f i = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)
[PROOFSTEP]
rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x : Fin a ⊕ Fin b, f (Equiv.toFun finSumFinEquiv x) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)
[PROOFSTEP]
apply Fintype.prod_sum_type
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (Equiv.toFun finSumFinEquiv (↑finSumFinEquiv.symm x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
x : Fin (a + b)
⊢ f x = f (Equiv.toFun finSumFinEquiv (↑finSumFinEquiv.symm x))
[PROOFSTEP]
simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i : Fin (a + b), f i = ∏ i : Fin a, f (castLE (_ : a ≤ a + b) i)
[PROOFSTEP]
rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i : Fin a, f (castAdd b i) = ∏ i : Fin a, f (castLE (_ : a ≤ a + b) i)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Monoid α
n : ℕ
f : Fin n → α
⊢ partialProd f 0 = 1
[PROOFSTEP]
simp [partialProd]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Monoid α
n : ℕ
f : Fin n → α
j : Fin n
⊢ partialProd f (succ j) = partialProd f (castSucc j) * f j
[PROOFSTEP]
simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt, ← Option.coe_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ partialProd f (succ j) = f 0 * partialProd (tail f) j
[PROOFSTEP]
simp [partialProd]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ f 0 * List.prod (List.take (↑j) (List.ofFn fun i => f (succ i))) =
    f 0 * List.prod (List.take (↑j) (List.ofFn (tail f)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x : Fin (n + 1)
⊢ (f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f (succ i)) 0 = f 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : (f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f (succ i)) (castSucc x) = f (castSucc x)
⊢ (f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f (succ i)) (succ x) = f (succ x)
[PROOFSTEP]
simp only [coe_eq_castSucc, Pi.smul_apply, smul_eq_mul] at hx ⊢
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i => (f (castSucc i))⁻¹ * f (succ i)) (castSucc x) = f (castSucc x)
⊢ f 0 * partialProd (fun i => (f (castSucc i))⁻¹ * f (succ i)) (succ x) = f (succ x)
[PROOFSTEP]
rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : Fin n
⊢ (partialProd f (castSucc i))⁻¹ * partialProd f (succ i) = f i
[PROOFSTEP]
cases' i with i hn
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn : i < n
⊢ (partialProd f (castSucc { val := i, isLt := hn }))⁻¹ * partialProd f (succ { val := i, isLt := hn }) =
    f { val := i, isLt := hn }
[PROOFSTEP]
induction i with
| zero => simp [-Fin.succ_mk, partialProd_succ]
| succ i hi =>
  specialize hi (lt_trans (Nat.lt_succ_self i) hn)
  simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi ⊢
  rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
  rw [Nat.succ_eq_add_one] at hn
  simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
    -- Porting note: was
        -- assoc_rw [hi, inv_mul_cancel_left]
  rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn : i < n
⊢ (partialProd f (castSucc { val := i, isLt := hn }))⁻¹ * partialProd f (succ { val := i, isLt := hn }) =
    f { val := i, isLt := hn }
[PROOFSTEP]
induction i with
| zero => simp [-Fin.succ_mk, partialProd_succ]
| succ i hi =>
  specialize hi (lt_trans (Nat.lt_succ_self i) hn)
  simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi ⊢
  rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
  rw [Nat.succ_eq_add_one] at hn
  simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
    -- Porting note: was
        -- assoc_rw [hi, inv_mul_cancel_left]
  rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
[GOAL]
case mk.zero
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
hn : Nat.zero < n
⊢ (partialProd f (castSucc { val := Nat.zero, isLt := hn }))⁻¹ * partialProd f (succ { val := Nat.zero, isLt := hn }) =
    f { val := Nat.zero, isLt := hn }
[PROOFSTEP]

| zero => simp [-Fin.succ_mk, partialProd_succ]
[GOAL]
case mk.zero
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
hn : Nat.zero < n
⊢ (partialProd f (castSucc { val := Nat.zero, isLt := hn }))⁻¹ * partialProd f (succ { val := Nat.zero, isLt := hn }) =
    f { val := Nat.zero, isLt := hn }
[PROOFSTEP]
simp [-Fin.succ_mk, partialProd_succ]
[GOAL]
case mk.succ
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hi :
  ∀ (hn : i < n),
    (partialProd f (castSucc { val := i, isLt := hn }))⁻¹ * partialProd f (succ { val := i, isLt := hn }) =
      f { val := i, isLt := hn }
hn : Nat.succ i < n
⊢ (partialProd f (castSucc { val := Nat.succ i, isLt := hn }))⁻¹ *
      partialProd f (succ { val := Nat.succ i, isLt := hn }) =
    f { val := Nat.succ i, isLt := hn }
[PROOFSTEP]

| succ i hi =>
  specialize hi (lt_trans (Nat.lt_succ_self i) hn)
  simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi ⊢
  rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
  rw [Nat.succ_eq_add_one] at hn
  simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
    -- Porting note: was
        -- assoc_rw [hi, inv_mul_cancel_left]
  rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
[GOAL]
case mk.succ
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hi :
  ∀ (hn : i < n),
    (partialProd f (castSucc { val := i, isLt := hn }))⁻¹ * partialProd f (succ { val := i, isLt := hn }) =
      f { val := i, isLt := hn }
hn : Nat.succ i < n
⊢ (partialProd f (castSucc { val := Nat.succ i, isLt := hn }))⁻¹ *
      partialProd f (succ { val := Nat.succ i, isLt := hn }) =
    f { val := Nat.succ i, isLt := hn }
[PROOFSTEP]
specialize hi (lt_trans (Nat.lt_succ_self i) hn)
[GOAL]
case mk.succ
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn : Nat.succ i < n
hi :
  (partialProd f (castSucc { val := i, isLt := (_ : i < n) }))⁻¹ *
      partialProd f (succ { val := i, isLt := (_ : i < n) }) =
    f { val := i, isLt := (_ : i < n) }
⊢ (partialProd f (castSucc { val := Nat.succ i, isLt := hn }))⁻¹ *
      partialProd f (succ { val := Nat.succ i, isLt := hn }) =
    f { val := Nat.succ i, isLt := hn }
[PROOFSTEP]
simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi ⊢
[GOAL]
case mk.succ
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn : Nat.succ i < n
hi :
  (partialProd f { val := i, isLt := (_ : i < Nat.succ n) })⁻¹ *
      partialProd f { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } =
    f { val := i, isLt := (_ : i < n) }
⊢ (partialProd f { val := Nat.succ i, isLt := (_ : Nat.succ i < Nat.succ n) })⁻¹ *
      partialProd f { val := Nat.succ i + 1, isLt := (_ : Nat.succ (Nat.succ i) < Nat.succ n) } =
    f { val := Nat.succ i, isLt := hn }
[PROOFSTEP]
rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
[GOAL]
case mk.succ
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn : Nat.succ i < n
hi :
  (partialProd f { val := i, isLt := (_ : i < Nat.succ n) })⁻¹ *
      partialProd f { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } =
    f { val := i, isLt := (_ : i < n) }
⊢ (partialProd f (succ { val := i, isLt := (_ : i < n) }))⁻¹ *
      partialProd f (succ { val := i + 1, isLt := ?mk.succ.h }) =
    f { val := Nat.succ i, isLt := hn }
case mk.succ.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn : Nat.succ i < n
hi :
  (partialProd f { val := i, isLt := (_ : i < Nat.succ n) })⁻¹ *
      partialProd f { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } =
    f { val := i, isLt := (_ : i < n) }
⊢ i + 1 < n
[PROOFSTEP]
rw [Nat.succ_eq_add_one] at hn
[GOAL]
case mk.succ
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn✝ : Nat.succ i < n
hn : i + 1 < n
hi :
  (partialProd f { val := i, isLt := (_ : i < Nat.succ n) })⁻¹ *
      partialProd f { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } =
    f { val := i, isLt := (_ : i < n) }
⊢ (partialProd f (succ { val := i, isLt := (_ : i < n) }))⁻¹ *
      partialProd f (succ { val := i + 1, isLt := (_ : i + 1 < n) }) =
    f { val := Nat.succ i, isLt := hn✝ }
[PROOFSTEP]
simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
  -- Porting note: was
      -- assoc_rw [hi, inv_mul_cancel_left]
[GOAL]
case mk.succ
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : ℕ
hn✝ : Nat.succ i < n
hn : i + 1 < n
hi :
  (partialProd f { val := i, isLt := (_ : i < Nat.succ n) })⁻¹ *
      partialProd f { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } =
    f { val := i, isLt := (_ : i < n) }
⊢ (f { val := i, isLt := (_ : i < n) })⁻¹ * (partialProd f { val := i, isLt := (_ : i < Nat.succ n) })⁻¹ *
      (partialProd f { val := i + 1, isLt := (_ : i + 1 < Nat.succ n) } * f { val := i + 1, isLt := (_ : i + 1 < n) }) =
    f { val := Nat.succ i, isLt := hn✝ }
[PROOFSTEP]
rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
⊢ (partialProd g (succAbove (succ j) (castSucc k)))⁻¹ * partialProd g (succ (succAbove j k)) =
    contractNth j (fun x x_1 => x * x_1) g k
[PROOFSTEP]
rcases lt_trichotomy (k : ℕ) j with (h | h | h)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ (partialProd g (succAbove (succ j) (castSucc k)))⁻¹ * partialProd g (succ (succAbove j k)) =
    contractNth j (fun x x_1 => x * x_1) g k
[PROOFSTEP]
rwa [succAbove_below, succAbove_below, partialProd_right_inv, contractNth_apply_of_lt]
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ castSucc k < j
[PROOFSTEP]
assumption
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ castSucc (castSucc k) < succ j
[PROOFSTEP]
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑(castSucc k) ≤ ↑j
[PROOFSTEP]
exact le_of_lt h
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ (partialProd g (succAbove (succ j) (castSucc k)))⁻¹ * partialProd g (succ (succAbove j k)) =
    contractNth j (fun x x_1 => x * x_1) g k
[PROOFSTEP]
rwa [succAbove_below, succAbove_above, partialProd_succ, castSucc_fin_succ, ← mul_assoc, partialProd_right_inv,
  contractNth_apply_of_eq]
[GOAL]
case inr.inl.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ castSucc k
[PROOFSTEP]
simp [le_iff_val_le_val, ← h]
[GOAL]
case inr.inl.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ castSucc (castSucc k) < succ j
[PROOFSTEP]
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
[GOAL]
case inr.inl.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ ↑(castSucc k) ≤ ↑j
[PROOFSTEP]
exact le_of_eq h
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ (partialProd g (succAbove (succ j) (castSucc k)))⁻¹ * partialProd g (succ (succAbove j k)) =
    contractNth j (fun x x_1 => x * x_1) g k
[PROOFSTEP]
rwa [succAbove_above, succAbove_above, partialProd_succ, partialProd_succ, castSucc_fin_succ, partialProd_succ,
  inv_mul_cancel_left, contractNth_apply_of_gt]
[GOAL]
case inr.inr.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ castSucc k
[PROOFSTEP]
exact le_iff_val_le_val.2 (le_of_lt h)
[GOAL]
case inr.inr.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ succ j ≤ castSucc (castSucc k)
[PROOFSTEP]
rw [le_iff_val_le_val, val_succ]
[GOAL]
case inr.inr.h
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ ↑j + 1 ≤ ↑(castSucc (castSucc k))
[PROOFSTEP]
exact Nat.succ_le_of_lt h
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
⊢ Fintype.card (Fin n → Fin m) = Fintype.card (Fin (m ^ n))
[PROOFSTEP]
simp_rw [Fintype.card_fun, Fintype.card_fin]
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
f : Fin n → Fin m
⊢ ∑ i : Fin n, ↑(f i) * m ^ ↑i < m ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
m n : ℕ
f✝ : Fin n → Fin m
f : Fin Nat.zero → Fin m
⊢ ∑ i : Fin Nat.zero, ↑(f i) * m ^ ↑i < m ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
m n✝ : ℕ
f✝ : Fin n✝ → Fin m
n : ℕ
ih : ∀ (f : Fin n → Fin m), ∑ i : Fin n, ↑(f i) * m ^ ↑i < m ^ n
f : Fin (Nat.succ n) → Fin m
⊢ ∑ i : Fin (Nat.succ n), ↑(f i) * m ^ ↑i < m ^ Nat.succ n
[PROOFSTEP]
cases m
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n✝ n : ℕ
f✝ : Fin n✝ → Fin Nat.zero
ih : ∀ (f : Fin n → Fin Nat.zero), ∑ i : Fin n, ↑(f i) * Nat.zero ^ ↑i < Nat.zero ^ n
f : Fin (Nat.succ n) → Fin Nat.zero
⊢ ∑ i : Fin (Nat.succ n), ↑(f i) * Nat.zero ^ ↑i < Nat.zero ^ Nat.succ n
[PROOFSTEP]
dsimp only [Nat.zero_eq] at f
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n✝ n : ℕ
f✝ : Fin n✝ → Fin Nat.zero
ih : ∀ (f : Fin n → Fin Nat.zero), ∑ i : Fin n, ↑(f i) * Nat.zero ^ ↑i < Nat.zero ^ n
f : Fin (Nat.succ n) → Fin 0
⊢ ∑ i : Fin (Nat.succ n), ↑(f i) * Nat.zero ^ ↑i < Nat.zero ^ Nat.succ n
[PROOFSTEP]
exact isEmptyElim (f <| Fin.last _)
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
n✝¹ n n✝ : ℕ
f✝ : Fin n✝¹ → Fin (Nat.succ n✝)
ih : ∀ (f : Fin n → Fin (Nat.succ n✝)), ∑ i : Fin n, ↑(f i) * Nat.succ n✝ ^ ↑i < Nat.succ n✝ ^ n
f : Fin (Nat.succ n) → Fin (Nat.succ n✝)
⊢ ∑ i : Fin (Nat.succ n), ↑(f i) * Nat.succ n✝ ^ ↑i < Nat.succ n✝ ^ Nat.succ n
[PROOFSTEP]
simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
n✝¹ n n✝ : ℕ
f✝ : Fin n✝¹ → Fin (Nat.succ n✝)
ih : ∀ (f : Fin n → Fin (Nat.succ n✝)), ∑ i : Fin n, ↑(f i) * Nat.succ n✝ ^ ↑i < Nat.succ n✝ ^ n
f : Fin (Nat.succ n) → Fin (Nat.succ n✝)
⊢ ∑ x : Fin n, ↑(f (Fin.castSucc x)) * Nat.succ n✝ ^ ↑x + ↑(f (Fin.last n)) * Nat.succ n✝ ^ n < Nat.succ n✝ ^ Nat.succ n
[PROOFSTEP]
refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
n✝¹ n n✝ : ℕ
f✝ : Fin n✝¹ → Fin (Nat.succ n✝)
ih : ∀ (f : Fin n → Fin (Nat.succ n✝)), ∑ i : Fin n, ↑(f i) * Nat.succ n✝ ^ ↑i < Nat.succ n✝ ^ n
f : Fin (Nat.succ n) → Fin (Nat.succ n✝)
⊢ Nat.succ n✝ ^ n + n✝ * Nat.succ n✝ ^ n = Nat.succ n✝ ^ Nat.succ n
[PROOFSTEP]
rw [← one_add_mul (_ : ℕ), add_comm, pow_succ]
  -- porting note: added, wrong `succ`
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
n✝¹ n n✝ : ℕ
f✝ : Fin n✝¹ → Fin (Nat.succ n✝)
ih : ∀ (f : Fin n → Fin (Nat.succ n✝)), ∑ i : Fin n, ↑(f i) * Nat.succ n✝ ^ ↑i < Nat.succ n✝ ^ n
f : Fin (Nat.succ n) → Fin (Nat.succ n✝)
⊢ (n✝ + 1) * Nat.succ n✝ ^ n = Nat.succ n✝ * Nat.succ n✝ ^ n
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
a : Fin (m ^ n)
b : Fin n
⊢ ↑a / m ^ ↑b % m < m
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u_1
β : Type u_2
m : ℕ
a : Fin (m ^ Nat.zero)
b : Fin Nat.zero
⊢ ↑a / m ^ ↑b % m < m
[PROOFSTEP]
exact b.elim0
[GOAL]
case succ
α : Type u_1
β : Type u_2
m n : ℕ
a : Fin (m ^ Nat.succ n)
b : Fin (Nat.succ n)
⊢ ↑a / m ^ ↑b % m < m
[PROOFSTEP]
cases' m with m
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n : ℕ
b : Fin (Nat.succ n)
a : Fin (Nat.zero ^ Nat.succ n)
⊢ ↑a / Nat.zero ^ ↑b % Nat.zero < Nat.zero
[PROOFSTEP]
dsimp only [Nat.zero_eq] at a
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n : ℕ
b : Fin (Nat.succ n)
a : Fin (0 ^ Nat.succ n)
⊢ ↑a / Nat.zero ^ ↑b % Nat.zero < Nat.zero
[PROOFSTEP]
rw [zero_pow n.succ_pos] at a
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n : ℕ
b : Fin (Nat.succ n)
a✝ : Fin (0 ^ Nat.succ n)
a : Fin 0
⊢ ↑a✝ / Nat.zero ^ ↑b % Nat.zero < Nat.zero
[PROOFSTEP]
exact a.elim0
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
n : ℕ
b : Fin (Nat.succ n)
m : ℕ
a : Fin (Nat.succ m ^ Nat.succ n)
⊢ ↑a / Nat.succ m ^ ↑b % Nat.succ m < Nat.succ m
[PROOFSTEP]
exact Nat.mod_lt _ m.succ_pos
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
a : Fin (m ^ n)
⊢ (fun f => { val := ∑ i : Fin n, ↑(f i) * m ^ ↑i, isLt := (_ : ∑ i : Fin n, ↑(f i) * m ^ ↑i < m ^ n) })
      ((fun a b => { val := ↑a / m ^ ↑b % m, isLt := (_ : ↑a / m ^ ↑b % m < m) }) a) =
    a
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
a : Fin (m ^ n)
⊢ { val := ∑ i : Fin n, ↑a / m ^ ↑i % m * m ^ ↑i,
      isLt := (_ : ∑ i : Fin n, ↑{ val := ↑a / m ^ ↑i % m, isLt := (_ : ↑a / m ^ ↑i % m < m) } * m ^ ↑i < m ^ n) } =
    a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
m n : ℕ
a✝ : Fin (m ^ n)
a : Fin (m ^ Nat.zero)
⊢ { val := ∑ i : Fin Nat.zero, ↑a / m ^ ↑i % m * m ^ ↑i,
      isLt :=
        (_ :
          ∑ i : Fin Nat.zero, ↑{ val := ↑a / m ^ ↑i % m, isLt := (_ : ↑a / m ^ ↑i % m < m) } * m ^ ↑i <
            m ^ Nat.zero) } =
    a
[PROOFSTEP]
haveI : Subsingleton (Fin (m ^ 0)) := (Fin.castIso <| pow_zero _).toEquiv.subsingleton
[GOAL]
case zero
α : Type u_1
β : Type u_2
m n : ℕ
a✝ : Fin (m ^ n)
a : Fin (m ^ Nat.zero)
this : Subsingleton (Fin (m ^ 0))
⊢ { val := ∑ i : Fin Nat.zero, ↑a / m ^ ↑i % m * m ^ ↑i,
      isLt :=
        (_ :
          ∑ i : Fin Nat.zero, ↑{ val := ↑a / m ^ ↑i % m, isLt := (_ : ↑a / m ^ ↑i % m < m) } * m ^ ↑i <
            m ^ Nat.zero) } =
    a
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case succ
α : Type u_1
β : Type u_2
m n✝ : ℕ
a✝ : Fin (m ^ n✝)
n : ℕ
ih :
  ∀ (a : Fin (m ^ n)),
    { val := ∑ i : Fin n, ↑a / m ^ ↑i % m * m ^ ↑i,
        isLt := (_ : ∑ i : Fin n, ↑{ val := ↑a / m ^ ↑i % m, isLt := (_ : ↑a / m ^ ↑i % m < m) } * m ^ ↑i < m ^ n) } =
      a
a : Fin (m ^ Nat.succ n)
⊢ { val := ∑ i : Fin (Nat.succ n), ↑a / m ^ ↑i % m * m ^ ↑i,
      isLt :=
        (_ :
          ∑ i : Fin (Nat.succ n), ↑{ val := ↑a / m ^ ↑i % m, isLt := (_ : ↑a / m ^ ↑i % m < m) } * m ^ ↑i <
            m ^ Nat.succ n) } =
    a
[PROOFSTEP]
simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
[GOAL]
case succ
α : Type u_1
β : Type u_2
m n✝ : ℕ
a✝ : Fin (m ^ n✝)
n : ℕ
a : Fin (m ^ Nat.succ n)
ih : ∀ (i : ℕ), i < m ^ n → ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i
⊢ { val := ∑ i : Fin (Nat.succ n), ↑a / m ^ ↑i % m * m ^ ↑i,
      isLt :=
        (_ :
          ∑ i : Fin (Nat.succ n), ↑{ val := ↑a / m ^ ↑i % m, isLt := (_ : ↑a / m ^ ↑i % m < m) } * m ^ ↑i <
            m ^ Nat.succ n) } =
    a
[PROOFSTEP]
ext
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
m n✝ : ℕ
a✝ : Fin (m ^ n✝)
n : ℕ
a : Fin (m ^ Nat.succ n)
ih : ∀ (i : ℕ), i < m ^ n → ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑{ val := ∑ i : Fin (Nat.succ n), ↑a / m ^ ↑i % m * m ^ ↑i,
        isLt :=
          (_ :
            ∑ i : Fin (Nat.succ n), ↑{ val := ↑a / m ^ ↑i % m, isLt := (_ : ↑a / m ^ ↑i % m < m) } * m ^ ↑i <
              m ^ Nat.succ n) } =
    ↑a
[PROOFSTEP]
simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one, mul_one, pow_succ, ←
  Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
m n✝ : ℕ
a✝ : Fin (m ^ n✝)
n : ℕ
a : Fin (m ^ Nat.succ n)
ih : ∀ (i : ℕ), i < m ^ n → ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a % m + m * ∑ x : Fin n, ↑a / m / m ^ ↑x % m * m ^ ↑x = ↑a
[PROOFSTEP]
rw [ih _ (Nat.div_lt_of_lt_mul ?_), Nat.mod_add_div]
  -- porting note: replaces `a.is_lt` in the wildcard above. Caused by a refactor of the `npow`
        -- instance for `Fin`.
[GOAL]
α : Type u_1
β : Type u_2
m n✝ : ℕ
a✝ : Fin (m ^ n✝)
n : ℕ
a : Fin (m ^ Nat.succ n)
ih : ∀ (i : ℕ), i < m ^ n → ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a < m * m ^ n
[PROOFSTEP]
exact a.is_lt.trans_eq (pow_succ _ _)
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(↑finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i
[PROOFSTEP]
rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0
[PROOFSTEP]
rintro x hx
[GOAL]
α : Type u_1
β : Type u_2
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
⊢ ↑(Pi.single i j x) * m ^ ↑x = 0
[PROOFSTEP]
rw [Pi.single_eq_of_ne hx, Fin.val_zero', zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ Fintype.card ((i : Fin m) → Fin (n i)) = Fintype.card (Fin (∏ i : Fin m, n i))
[PROOFSTEP]
simp_rw [Fintype.card_pi, Fintype.card_fin]
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
⊢ ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
f✝ : (i : Fin m) → Fin (n✝ i)
n : Fin Nat.zero → ℕ
f : (i : Fin Nat.zero) → Fin (n i)
⊢ ∑ i : Fin Nat.zero, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ Nat.zero) j) < ∏ i : Fin Nat.zero, n i
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
⊢ ∑ i : Fin (Nat.succ m), ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ Nat.succ m) j) < ∏ i : Fin (Nat.succ m), n i
[PROOFSTEP]
rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
case succ
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
⊢ ∑ i : Fin m,
        ↑(f (Fin.castSucc i)) * ∏ j : Fin ↑(Fin.castSucc i), n (Fin.castLE (_ : ↑(Fin.castSucc i) ≤ Nat.succ m) j) +
      ↑(f (Fin.last m)) * ∏ j : Fin ↑(Fin.last m), n (Fin.castLE (_ : ↑(Fin.last m) ≤ Nat.succ m) j) <
    (∏ i : Fin m, n (Fin.castSucc i)) * n (Fin.last m)
[PROOFSTEP]
suffices
  ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
    ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) < (∏ i : Fin m, n i) * nn
  by
  replace := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
  rw [← Fin.snoc_init_self f]
  simp (config := { singlePass := true }) only [← Fin.snoc_init_self n]
  simp_rw [Fin.snoc_castSucc, Fin.snoc_last, Fin.snoc_init_self n]
  exact this
[GOAL]
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
this :
  ∀ (n : Fin m → ℕ) (nn : ℕ) (f : (i : Fin m) → Fin (n i)) (fn : Fin nn),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) + ↑fn * ∏ j : Fin m, n j < (∏ i : Fin m, n i) * nn
⊢ ∑ i : Fin m,
        ↑(f (Fin.castSucc i)) * ∏ j : Fin ↑(Fin.castSucc i), n (Fin.castLE (_ : ↑(Fin.castSucc i) ≤ Nat.succ m) j) +
      ↑(f (Fin.last m)) * ∏ j : Fin ↑(Fin.last m), n (Fin.castLE (_ : ↑(Fin.last m) ≤ Nat.succ m) j) <
    (∏ i : Fin m, n (Fin.castSucc i)) * n (Fin.last m)
[PROOFSTEP]
replace := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
[GOAL]
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
this :
  ∑ i : Fin m, ↑(Fin.init f i) * ∏ j : Fin ↑i, Fin.init n (Fin.castLE (_ : ↑i ≤ m) j) +
      ↑(f (Fin.last m)) * ∏ j : Fin m, Fin.init n j <
    (∏ i : Fin m, Fin.init n i) * n (Fin.last m)
⊢ ∑ i : Fin m,
        ↑(f (Fin.castSucc i)) * ∏ j : Fin ↑(Fin.castSucc i), n (Fin.castLE (_ : ↑(Fin.castSucc i) ≤ Nat.succ m) j) +
      ↑(f (Fin.last m)) * ∏ j : Fin ↑(Fin.last m), n (Fin.castLE (_ : ↑(Fin.last m) ≤ Nat.succ m) j) <
    (∏ i : Fin m, n (Fin.castSucc i)) * n (Fin.last m)
[PROOFSTEP]
rw [← Fin.snoc_init_self f]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
this :
  ∑ i : Fin m, ↑(Fin.init f i) * ∏ j : Fin ↑i, Fin.init n (Fin.castLE (_ : ↑i ≤ m) j) +
      ↑(f (Fin.last m)) * ∏ j : Fin m, Fin.init n j <
    (∏ i : Fin m, Fin.init n i) * n (Fin.last m)
⊢ ∑ i : Fin m,
        ↑(Fin.snoc (Fin.init f) (f (Fin.last m)) (Fin.castSucc i)) *
          ∏ j : Fin ↑(Fin.castSucc i), n (Fin.castLE (_ : ↑(Fin.castSucc i) ≤ Nat.succ m) j) +
      ↑(Fin.snoc (Fin.init f) (f (Fin.last m)) (Fin.last m)) *
        ∏ j : Fin ↑(Fin.last m), n (Fin.castLE (_ : ↑(Fin.last m) ≤ Nat.succ m) j) <
    (∏ i : Fin m, n (Fin.castSucc i)) * n (Fin.last m)
[PROOFSTEP]
simp (config := { singlePass := true }) only [← Fin.snoc_init_self n]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
this :
  ∑ i : Fin m, ↑(Fin.init f i) * ∏ j : Fin ↑i, Fin.init n (Fin.castLE (_ : ↑i ≤ m) j) +
      ↑(f (Fin.last m)) * ∏ j : Fin m, Fin.init n j <
    (∏ i : Fin m, Fin.init n i) * n (Fin.last m)
⊢ ∑ x : Fin m,
        ↑(Fin.snoc (Fin.init f) (f (Fin.last m)) (Fin.castSucc x)) *
          ∏ x_1 : Fin ↑(Fin.castSucc x),
            Fin.snoc (Fin.init n) (n (Fin.last m)) (Fin.castLE (_ : ↑(Fin.castSucc x) ≤ Nat.succ m) x_1) +
      ↑(Fin.snoc (Fin.init f) (f (Fin.last m)) (Fin.last m)) *
        ∏ x : Fin ↑(Fin.last m),
          Fin.snoc (Fin.init n) (n (Fin.last m)) (Fin.castLE (_ : ↑(Fin.last m) ≤ Nat.succ m) x) <
    (∏ x : Fin m, Fin.snoc (Fin.init n) (n (Fin.last m)) (Fin.castSucc x)) *
      Fin.snoc (Fin.init n) (n (Fin.last m)) (Fin.last m)
[PROOFSTEP]
simp_rw [Fin.snoc_castSucc, Fin.snoc_last, Fin.snoc_init_self n]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
this :
  ∑ i : Fin m, ↑(Fin.init f i) * ∏ j : Fin ↑i, Fin.init n (Fin.castLE (_ : ↑i ≤ m) j) +
      ↑(f (Fin.last m)) * ∏ j : Fin m, Fin.init n j <
    (∏ i : Fin m, Fin.init n i) * n (Fin.last m)
⊢ ∑ x : Fin m,
        ↑(Fin.init f x) * ∏ x_1 : Fin ↑(Fin.castSucc x), n (Fin.castLE (_ : ↑(Fin.castSucc x) ≤ Nat.succ m) x_1) +
      ↑(f (Fin.last m)) * ∏ x : Fin ↑(Fin.last m), n (Fin.castLE (_ : ↑(Fin.last m) ≤ Nat.succ m) x) <
    (∏ x : Fin m, Fin.init n x) * n (Fin.last m)
[PROOFSTEP]
exact this
[GOAL]
case succ
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝ : Fin m✝ → ℕ
f✝ : (i : Fin m✝) → Fin (n✝ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n : Fin (Nat.succ m) → ℕ
f : (i : Fin (Nat.succ m)) → Fin (n i)
⊢ ∀ (n : Fin m → ℕ) (nn : ℕ) (f : (i : Fin m) → Fin (n i)) (fn : Fin nn),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) + ↑fn * ∏ j : Fin m, n j < (∏ i : Fin m, n i) * nn
[PROOFSTEP]
intro n nn f fn
[GOAL]
case succ
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝¹ : Fin m✝ → ℕ
f✝¹ : (i : Fin m✝) → Fin (n✝¹ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n✝ : Fin (Nat.succ m) → ℕ
f✝ : (i : Fin (Nat.succ m)) → Fin (n✝ i)
n : Fin m → ℕ
nn : ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin nn
⊢ ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) + ↑fn * ∏ j : Fin m, n j < (∏ i : Fin m, n i) * nn
[PROOFSTEP]
cases nn
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝¹ : Fin m✝ → ℕ
f✝¹ : (i : Fin m✝) → Fin (n✝¹ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n✝ : Fin (Nat.succ m) → ℕ
f✝ : (i : Fin (Nat.succ m)) → Fin (n✝ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin Nat.zero
⊢ ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) + ↑fn * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * Nat.zero
[PROOFSTEP]
dsimp only [Nat.zero_eq] at fn
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝¹ : Fin m✝ → ℕ
f✝¹ : (i : Fin m✝) → Fin (n✝¹ i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n✝ : Fin (Nat.succ m) → ℕ
f✝ : (i : Fin (Nat.succ m)) → Fin (n✝ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin 0
⊢ ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) + ↑fn * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * Nat.zero
[PROOFSTEP]
exact isEmptyElim fn
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝² : Fin m✝ → ℕ
f✝¹ : (i : Fin m✝) → Fin (n✝² i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n✝¹ : Fin (Nat.succ m) → ℕ
f✝ : (i : Fin (Nat.succ m)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (Nat.succ n✝)
⊢ ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) + ↑fn * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * Nat.succ n✝
[PROOFSTEP]
refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝² : Fin m✝ → ℕ
f✝¹ : (i : Fin m✝) → Fin (n✝² i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n✝¹ : Fin (Nat.succ m) → ℕ
f✝ : (i : Fin (Nat.succ m)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (Nat.succ n✝)
⊢ ∏ i : Fin m, n i + n✝ * ∏ j : Fin m, n j = (∏ i : Fin m, n i) * Nat.succ n✝
[PROOFSTEP]
rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]
  -- porting note: added, wrong `succ`
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
m✝ : ℕ
n✝² : Fin m✝ → ℕ
f✝¹ : (i : Fin m✝) → Fin (n✝² i)
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i
n✝¹ : Fin (Nat.succ m) → ℕ
f✝ : (i : Fin (Nat.succ m)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (Nat.succ n✝)
⊢ (∏ i : Fin m, n i) * (n✝ + 1) = (∏ i : Fin m, n i) * Nat.succ n✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin m, n i)
b : Fin m
⊢ (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ m) j)) % n b < n b
[PROOFSTEP]
cases m
[GOAL]
case zero
α : Type u_1
β : Type u_2
n : Fin Nat.zero → ℕ
a : Fin (∏ i : Fin Nat.zero, n i)
b : Fin Nat.zero
⊢ (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ Nat.zero) j)) % n b < n b
[PROOFSTEP]
exact b.elim0
[GOAL]
case succ
α : Type u_1
β : Type u_2
n✝ : ℕ
n : Fin (Nat.succ n✝) → ℕ
a : Fin (∏ i : Fin (Nat.succ n✝), n i)
b : Fin (Nat.succ n✝)
⊢ (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ Nat.succ n✝) j)) % n b < n b
[PROOFSTEP]
cases' h : n b with nb
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n✝ : ℕ
n : Fin (Nat.succ n✝) → ℕ
a : Fin (∏ i : Fin (Nat.succ n✝), n i)
b : Fin (Nat.succ n✝)
h : n b = Nat.zero
⊢ (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ Nat.succ n✝) j)) % Nat.zero < Nat.zero
[PROOFSTEP]
rw [prod_eq_zero (Finset.mem_univ _) h] at a
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n✝ : ℕ
n : Fin (Nat.succ n✝) → ℕ
a✝ : Fin (∏ i : Fin (Nat.succ n✝), n i)
a : Fin 0
b : Fin (Nat.succ n✝)
h : n b = Nat.zero
⊢ (↑a✝ / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ Nat.succ n✝) j)) % Nat.zero < Nat.zero
[PROOFSTEP]
exact isEmptyElim a
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
n✝ : ℕ
n : Fin (Nat.succ n✝) → ℕ
a : Fin (∏ i : Fin (Nat.succ n✝), n i)
b : Fin (Nat.succ n✝)
nb : ℕ
h : n b = Nat.succ nb
⊢ (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ Nat.succ n✝) j)) % Nat.succ nb < Nat.succ nb
[PROOFSTEP]
exact Nat.mod_lt _ nb.succ_pos
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ Function.RightInverse
    (fun a b =>
      { val := (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ m) j)) % n b,
        isLt := (_ : (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ m) j)) % n b < n b) })
    fun f =>
    { val := ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j),
      isLt := (_ : ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i) }
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin m, n i)
⊢ (fun f =>
        { val := ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j),
          isLt := (_ : ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i) })
      ((fun a b =>
          { val := (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ m) j)) % n b,
            isLt := (_ : (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ m) j)) % n b < n b) })
        a) =
    a
[PROOFSTEP]
revert a
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i : Fin m, n i)),
    (fun f =>
          { val := ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j),
            isLt := (_ : ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) < ∏ i : Fin m, n i) })
        ((fun a b =>
            { val := (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ m) j)) % n b,
              isLt := (_ : (↑a / ∏ j : Fin ↑b, n (Fin.castLE (_ : ↑b ≤ m) j)) % n b < n b) })
          a) =
      a
[PROOFSTEP]
dsimp only [Fin.val_mk]
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i : Fin m, n i)),
    {
        val :=
          ∑ i : Fin m,
            (↑a / ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j)) % n i * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j),
        isLt :=
          (_ :
            ∑ i : Fin m,
                ↑{ val := (↑a / ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j)) % n i,
                      isLt := (_ : (↑a / ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j)) % n i < n i) } *
                  ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j) <
              ∏ i : Fin m, n i) } =
      a
[PROOFSTEP]
refine' Fin.consInduction _ _ n
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i : Fin 0, Fin.elim0 i)),
    {
        val :=
          ∑ i : Fin 0,
            (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i *
              ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j),
        isLt :=
          (_ :
            ∑ i : Fin 0,
                ↑{ val := (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i,
                      isLt :=
                        (_ : (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i < Fin.elim0 i) } *
                  ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j) <
              ∏ i : Fin 0, Fin.elim0 i) } =
      a
[PROOFSTEP]
intro a
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin 0, Fin.elim0 i)
⊢ {
      val :=
        ∑ i : Fin 0,
          (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i *
            ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j),
      isLt :=
        (_ :
          ∑ i : Fin 0,
              ↑{ val := (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i,
                    isLt :=
                      (_ : (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i < Fin.elim0 i) } *
                ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j) <
            ∏ i : Fin 0, Fin.elim0 i) } =
    a
[PROOFSTEP]
haveI : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) := (Fin.castIso <| prod_empty).toEquiv.subsingleton
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin 0, Fin.elim0 i)
this : Subsingleton (Fin (∏ i : Fin 0, Fin.elim0 i))
⊢ {
      val :=
        ∑ i : Fin 0,
          (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i *
            ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j),
      isLt :=
        (_ :
          ∑ i : Fin 0,
              ↑{ val := (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i,
                    isLt :=
                      (_ : (↑a / ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j)) % Fin.elim0 i < Fin.elim0 i) } *
                ∏ j : Fin ↑i, Fin.elim0 (Fin.castLE (_ : ↑i ≤ 0) j) <
            ∏ i : Fin 0, Fin.elim0 i) } =
    a
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ {n : ℕ} (x₀ : ℕ) (x : Fin n → ℕ),
    (∀ (a : Fin (∏ i : Fin n, x i)),
        {
            val :=
              ∑ i : Fin n,
                (↑a / ∏ j : Fin ↑i, x (Fin.castLE (_ : ↑i ≤ n) j)) % x i * ∏ j : Fin ↑i, x (Fin.castLE (_ : ↑i ≤ n) j),
            isLt :=
              (_ :
                ∑ i : Fin n,
                    ↑{ val := (↑a / ∏ j : Fin ↑i, x (Fin.castLE (_ : ↑i ≤ n) j)) % x i,
                          isLt := (_ : (↑a / ∏ j : Fin ↑i, x (Fin.castLE (_ : ↑i ≤ n) j)) % x i < x i) } *
                      ∏ j : Fin ↑i, x (Fin.castLE (_ : ↑i ≤ n) j) <
                  ∏ i : Fin n, x i) } =
          a) →
      ∀ (a : Fin (∏ i : Fin (n + 1), Fin.cons x₀ x i)),
        {
            val :=
              ∑ i : Fin (n + 1),
                (↑a / ∏ j : Fin ↑i, Fin.cons x₀ x (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x₀ x i *
                  ∏ j : Fin ↑i, Fin.cons x₀ x (Fin.castLE (_ : ↑i ≤ n + 1) j),
            isLt :=
              (_ :
                ∑ i : Fin (n + 1),
                    ↑{ val := (↑a / ∏ j : Fin ↑i, Fin.cons x₀ x (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x₀ x i,
                          isLt :=
                            (_ :
                              (↑a / ∏ j : Fin ↑i, Fin.cons x₀ x (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x₀ x i <
                                Fin.cons x₀ x i) } *
                      ∏ j : Fin ↑i, Fin.cons x₀ x (Fin.castLE (_ : ↑i ≤ n + 1) j) <
                  ∏ i : Fin (n + 1), Fin.cons x₀ x i) } =
          a
[PROOFSTEP]
intro n x xs ih a
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
ih :
  ∀ (a : Fin (∏ i : Fin n, xs i)),
    {
        val :=
          ∑ i : Fin n,
            (↑a / ∏ j : Fin ↑i, xs (Fin.castLE (_ : ↑i ≤ n) j)) % xs i * ∏ j : Fin ↑i, xs (Fin.castLE (_ : ↑i ≤ n) j),
        isLt :=
          (_ :
            ∑ i : Fin n,
                ↑{ val := (↑a / ∏ j : Fin ↑i, xs (Fin.castLE (_ : ↑i ≤ n) j)) % xs i,
                      isLt := (_ : (↑a / ∏ j : Fin ↑i, xs (Fin.castLE (_ : ↑i ≤ n) j)) % xs i < xs i) } *
                  ∏ j : Fin ↑i, xs (Fin.castLE (_ : ↑i ≤ n) j) <
              ∏ i : Fin n, xs i) } =
      a
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
⊢ {
      val :=
        ∑ i : Fin (n + 1),
          (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i *
            ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j),
      isLt :=
        (_ :
          ∑ i : Fin (n + 1),
              ↑{ val := (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i,
                    isLt :=
                      (_ :
                        (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i <
                          Fin.cons x xs i) } *
                ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j) <
            ∏ i : Fin (n + 1), Fin.cons x xs i) } =
    a
[PROOFSTEP]
simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ {
      val :=
        ∑ i : Fin (n + 1),
          (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i *
            ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j),
      isLt :=
        (_ :
          ∑ i : Fin (n + 1),
              ↑{ val := (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i,
                    isLt :=
                      (_ :
                        (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i <
                          Fin.cons x xs i) } *
                ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j) <
            ∏ i : Fin (n + 1), Fin.cons x xs i) } =
    a
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ ↑{
        val :=
          ∑ i : Fin (n + 1),
            (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i *
              ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j),
        isLt :=
          (_ :
            ∑ i : Fin (n + 1),
                ↑{ val := (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i,
                      isLt :=
                        (_ :
                          (↑a / ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j)) % Fin.cons x xs i <
                            Fin.cons x xs i) } *
                  ∏ j : Fin ↑i, Fin.cons x xs (Fin.castLE (_ : ↑i ≤ n + 1) j) <
              ∏ i : Fin (n + 1), Fin.cons x xs i) } =
    ↑a
[PROOFSTEP]
simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ (↑a / ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j)) % Fin.cons x xs 0 *
        ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j) +
      ∑ x_1 : Fin n,
        (↑a / ∏ j : Fin ↑(Fin.succ x_1), Fin.cons x xs (Fin.castLE (_ : ↑(Fin.succ x_1) ≤ n + 1) j)) % xs x_1 *
          ∏ j : Fin ↑(Fin.succ x_1), Fin.cons x xs (Fin.castLE (_ : ↑(Fin.succ x_1) ≤ n + 1) j) =
    ↑a
[PROOFSTEP]
have := fun i : Fin n =>
  Fintype.prod_equiv (Fin.castIso <| Fin.val_succ i).toEquiv
    (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
    (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j)) fun j => rfl
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
this :
  ∀ (i : Fin n),
    ∏ x_1 : Fin ↑(Fin.succ i), Fin.cons x xs (Fin.castLE (_ : ↑(Fin.succ i) ≤ n + 1) x_1) =
      ∏ x_1 : Fin (↑i + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑i ≤ Nat.succ n) x_1)
⊢ (↑a / ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j)) % Fin.cons x xs 0 *
        ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j) +
      ∑ x_1 : Fin n,
        (↑a / ∏ j : Fin ↑(Fin.succ x_1), Fin.cons x xs (Fin.castLE (_ : ↑(Fin.succ x_1) ≤ n + 1) j)) % xs x_1 *
          ∏ j : Fin ↑(Fin.succ x_1), Fin.cons x xs (Fin.castLE (_ : ↑(Fin.succ x_1) ≤ n + 1) j) =
    ↑a
[PROOFSTEP]
simp_rw [this]
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
this :
  ∀ (i : Fin n),
    ∏ x_1 : Fin ↑(Fin.succ i), Fin.cons x xs (Fin.castLE (_ : ↑(Fin.succ i) ≤ n + 1) x_1) =
      ∏ x_1 : Fin (↑i + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑i ≤ Nat.succ n) x_1)
⊢ (↑a / ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j)) % Fin.cons x xs 0 *
        ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j) +
      ∑ x_1 : Fin n,
        (↑a / ∏ x_2 : Fin (↑x_1 + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) x_2)) % xs x_1 *
          ∏ x_2 : Fin (↑x_1 + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) x_2) =
    ↑a
[PROOFSTEP]
clear this
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ (↑a / ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j)) % Fin.cons x xs 0 *
        ∏ j : Fin ↑0, Fin.cons x xs (Fin.castLE (_ : ↑0 ≤ n + 1) j) +
      ∑ x_1 : Fin n,
        (↑a / ∏ x_2 : Fin (↑x_1 + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) x_2)) % xs x_1 *
          ∏ x_2 : Fin (↑x_1 + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) x_2) =
    ↑a
[PROOFSTEP]
dsimp only [Fin.val_zero]
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ (↑a / ∏ j : Fin 0, Fin.cons x xs (Fin.castLE (_ : 0 ≤ n + 1) j)) % Fin.cons x xs 0 *
        ∏ j : Fin 0, Fin.cons x xs (Fin.castLE (_ : 0 ≤ n + 1) j) +
      ∑ x_1 : Fin n,
        (↑a / ∏ x_2 : Fin (↑x_1 + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) x_2)) % xs x_1 *
          ∏ x_2 : Fin (↑x_1 + 1), Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) x_2) =
    ↑a
[PROOFSTEP]
simp_rw [Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero, Fin.prod_univ_succ]
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ ↑a % x +
      ∑ x_1 : Fin n,
        ↑a /
              (Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) 0) *
                ∏ i : Fin ↑x_1, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) (Fin.succ i))) %
            xs x_1 *
          (Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) 0) *
            ∏ i : Fin ↑x_1, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) (Fin.succ i))) =
    ↑a
[PROOFSTEP]
change (_ + ∑ y : _, _ / (x * _) % _ * (x * _)) = _
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ ↑a % x +
      ∑ y : Fin n,
        ↑a / (x * ∏ i : Fin ↑y, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑y ≤ Nat.succ n) (Fin.succ i))) % xs y *
          (x * ∏ i : Fin ↑y, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑y ≤ Nat.succ n) (Fin.succ i))) =
    ↑a
[PROOFSTEP]
simp_rw [← Nat.div_div_eq_div_mul, mul_left_comm (_ % _ : ℕ), ← mul_sum]
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ ↑a % x +
      x *
        ∑ x_1 : Fin n,
          (↑a / x / ∏ i : Fin ↑x_1, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) (Fin.succ i))) % xs x_1 *
            ∏ i : Fin ↑x_1, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) (Fin.succ i)) =
    ↑a
[PROOFSTEP]
convert
  Nat.mod_add_div _
    _
      -- porting note: new
[GOAL]
case h.e'_2.h.e'_6.h.e'_6
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ ∑ x_1 : Fin n,
      (↑a / x / ∏ i : Fin ↑x_1, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) (Fin.succ i))) % xs x_1 *
        ∏ i : Fin ↑x_1, Fin.cons x xs (Fin.castLE (_ : Nat.succ ↑x_1 ≤ Nat.succ n) (Fin.succ i)) =
    ↑a / x
[PROOFSTEP]
refine (ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq ?_))
[GOAL]
case h.e'_2.h.e'_6.h.e'_6
α : Type u_1
β : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons x xs i)
ih :
  ∀ (i : ℕ),
    i < ∏ i : Fin n, xs i →
      ∑ x : Fin n,
          (i / ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j)) % xs x * ∏ j : Fin ↑x, xs (Fin.castLE (_ : ↑x ≤ n) j) =
        i
⊢ ∏ i : Fin (n + 1), Fin.cons x xs i = x * ∏ i : Fin n, xs i
[PROOFSTEP]
exact
  Fin.prod_univ_succ
    _  -- porting note: was:
              /-
              refine' Eq.trans _ (ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq _))
              swap
              · convert Fin.prod_univ_succ (Fin.cons x xs : ∀ _, ℕ)
                simp_rw [Fin.cons_succ]
              congr with i
              congr with j
              · cases j
                rfl
              · cases j
                rfl-/
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑(↑finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j : Fin ↑i, n (Fin.castLE (_ : ↑i ≤ m) j)
[PROOFSTEP]
rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE (_ : ↑x ≤ m) j) = 0
[PROOFSTEP]
rintro x hx
[GOAL]
α : Type u_1
β : Type u_2
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
⊢ ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE (_ : ↑x ≤ m) j) = 0
[PROOFSTEP]
rw [Pi.single_eq_of_ne hx, Fin.val_zero', zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
⊢ prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
[PROOFSTEP]
induction i with
| zero => simp
| succ i IH =>
  by_cases h : i < n
  · have : i < length (ofFn f) := by rwa [length_ofFn f]
    rw [prod_take_succ _ _ this]
    have A :
      ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i + 1) =
        ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i) ∪ {(⟨i, h⟩ : Fin n)} :=
      by
      ext ⟨_, _⟩
      simp [Nat.lt_succ_iff_lt_or_eq]
    have B : _root_.Disjoint (Finset.filter (fun j : Fin n => j.val < i) Finset.univ) (singleton (⟨i, h⟩ : Fin n)) := by
      simp
    rw [A, Finset.prod_union B, IH]
    simp
  · have A : (ofFn f).take i = (ofFn f).take i.succ :=
      by
      rw [← length_ofFn f] at h
      have : length (ofFn f) ≤ i := not_lt.mp h
      rw [take_all_of_le this, take_all_of_le (le_trans this (Nat.le_succ _))]
    have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) :=
      by
      intro j
      have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
      simp [this, lt_trans this (Nat.lt_succ_self _)]
    simp [← A, B, IH]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
⊢ prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
[PROOFSTEP]
induction i with
| zero => simp
| succ i IH =>
  by_cases h : i < n
  · have : i < length (ofFn f) := by rwa [length_ofFn f]
    rw [prod_take_succ _ _ this]
    have A :
      ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i + 1) =
        ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i) ∪ {(⟨i, h⟩ : Fin n)} :=
      by
      ext ⟨_, _⟩
      simp [Nat.lt_succ_iff_lt_or_eq]
    have B : _root_.Disjoint (Finset.filter (fun j : Fin n => j.val < i) Finset.univ) (singleton (⟨i, h⟩ : Fin n)) := by
      simp
    rw [A, Finset.prod_union B, IH]
    simp
  · have A : (ofFn f).take i = (ofFn f).take i.succ :=
      by
      rw [← length_ofFn f] at h
      have : length (ofFn f) ≤ i := not_lt.mp h
      rw [take_all_of_le this, take_all_of_le (le_trans this (Nat.le_succ _))]
    have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) :=
      by
      intro j
      have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
      simp [this, lt_trans this (Nat.lt_succ_self _)]
    simp [← A, B, IH]
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ prod (take Nat.zero (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.zero) univ, f j
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ prod (take Nat.zero (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.zero) univ, f j
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]

| succ i IH =>
  by_cases h : i < n
  · have : i < length (ofFn f) := by rwa [length_ofFn f]
    rw [prod_take_succ _ _ this]
    have A :
      ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i + 1) =
        ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i) ∪ {(⟨i, h⟩ : Fin n)} :=
      by
      ext ⟨_, _⟩
      simp [Nat.lt_succ_iff_lt_or_eq]
    have B : _root_.Disjoint (Finset.filter (fun j : Fin n => j.val < i) Finset.univ) (singleton (⟨i, h⟩ : Fin n)) := by
      simp
    rw [A, Finset.prod_union B, IH]
    simp
  · have A : (ofFn f).take i = (ofFn f).take i.succ :=
      by
      rw [← length_ofFn f] at h
      have : length (ofFn f) ≤ i := not_lt.mp h
      rw [take_all_of_le this, take_all_of_le (le_trans this (Nat.le_succ _))]
    have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) :=
      by
      intro j
      have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
      simp [this, lt_trans this (Nat.lt_succ_self _)]
    simp [← A, B, IH]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
by_cases h : i < n
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
have : i < length (ofFn f) := by rwa [length_ofFn f]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
⊢ i < length (ofFn f)
[PROOFSTEP]
rwa [length_ofFn f]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
rw [prod_take_succ _ _ this]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
have A :
  ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i + 1) =
    ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i) ∪ {(⟨i, h⟩ : Fin n)} :=
  by
  ext ⟨_, _⟩
  simp [Nat.lt_succ_iff_lt_or_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
[PROOFSTEP]
ext ⟨_, _⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
val✝ : ℕ
isLt✝ : val✝ < n
⊢ { val := val✝, isLt := isLt✝ } ∈ Finset.filter (fun j => ↑j < i + 1) univ ↔
    { val := val✝, isLt := isLt✝ } ∈ Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
[PROOFSTEP]
simp [Nat.lt_succ_iff_lt_or_eq]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
have B : _root_.Disjoint (Finset.filter (fun j : Fin n => j.val < i) Finset.univ) (singleton (⟨i, h⟩ : Fin n)) := by
  simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
⊢ _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
rw [A, Finset.prod_union B, IH]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
⊢ (∏ j in Finset.filter (fun j => ↑j < i) univ, f j) * nthLe (ofFn f) i this =
    (∏ x in Finset.filter (fun j => ↑j < i) univ, f x) * ∏ x in {{ val := i, isLt := h }}, f x
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
have A : (ofFn f).take i = (ofFn f).take i.succ :=
  by
  rw [← length_ofFn f] at h
  have : length (ofFn f) ≤ i := not_lt.mp h
  rw [take_all_of_le this, take_all_of_le (le_trans this (Nat.le_succ _))]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
[PROOFSTEP]
rw [← length_ofFn f] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < length (ofFn f)
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
[PROOFSTEP]
have : length (ofFn f) ≤ i := not_lt.mp h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < length (ofFn f)
this : length (ofFn f) ≤ i
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
[PROOFSTEP]
rw [take_all_of_le this, take_all_of_le (le_trans this (Nat.le_succ _))]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) :=
  by
  intro j
  have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
  simp [this, lt_trans this (Nat.lt_succ_self _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
⊢ ∀ (j : Fin n), (↑j < Nat.succ i) = (↑j < i)
[PROOFSTEP]
intro j
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
j : Fin n
⊢ (↑j < Nat.succ i) = (↑j < i)
[PROOFSTEP]
have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
j : Fin n
this : ↑j < i
⊢ (↑j < Nat.succ i) = (↑j < i)
[PROOFSTEP]
simp [this, lt_trans this (Nat.lt_succ_self _)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
B : ∀ (j : Fin n), (↑j < Nat.succ i) = (↑j < i)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
[PROOFSTEP]
simp [← A, B, IH]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ prod (ofFn f) = ∏ i : Fin n, f i
[PROOFSTEP]
convert prod_take_ofFn f n
[GOAL]
case h.e'_2.h.e'_4
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ ofFn f = take n (ofFn f)
[PROOFSTEP]
rw [take_all_of_le (le_of_eq (length_ofFn f))]
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ univ = Finset.filter (fun j => ↑j < n) univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
⊢ alternatingProd [] = ∏ i : Fin (length []), get [] i ^ (-1) ^ ↑i
[PROOFSTEP]
rw [alternatingProd, Finset.prod_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
⊢ ∀ (x : Fin (length [])), x ∈ univ → get [] x ^ (-1) ^ ↑x = 1
[PROOFSTEP]
rintro ⟨i, ⟨⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ alternatingProd [g] = ∏ i : Fin (length [g]), get [g] i ^ (-1) ^ ↑i
[PROOFSTEP]
show g = ∏ i : Fin 1, [g].get i ^ (-1 : ℤ) ^ (i : ℕ)
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ g = ∏ i : Fin 1, get [g] i ^ (-1) ^ ↑i
[PROOFSTEP]
rw [Fin.prod_univ_succ]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ g = get [g] 0 ^ (-1) ^ ↑0 * ∏ i : Fin 0, get [g] (Fin.succ i) ^ (-1) ^ ↑(Fin.succ i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i : Fin (length L), get L i ^ (-1) ^ ↑i = ∏ i : Fin (length L + 2), get (g :: h :: L) i ^ (-1) ^ ↑i
[PROOFSTEP]
{ rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
  simp [Nat.succ_eq_add_one, pow_add]
}
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i : Fin (length L), get L i ^ (-1) ^ ↑i = ∏ i : Fin (length L + 2), get (g :: h :: L) i ^ (-1) ^ ↑i
[PROOFSTEP]
rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
g h : G
L : List G
⊢ g * (h⁻¹ * ∏ i : Fin (length L), get L i ^ (-1) ^ ↑i) =
    get (g :: h :: L) 0 ^ (-1) ^ ↑0 *
      (get (g :: h :: L) (Fin.succ 0) ^ (-1) ^ ↑(Fin.succ 0) *
        ∏ i : Fin (length L), get (g :: h :: L) (Fin.succ (Fin.succ i)) ^ (-1) ^ ↑(Fin.succ (Fin.succ i)))
[PROOFSTEP]
simp [Nat.succ_eq_add_one, pow_add]


[GOAL]
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
inst✝⁴ : Semiring S✝
inst✝³ : AddCommMonoid M✝
inst✝² : CommSemiring R
inst✝¹ : Algebra R S✝
inst✝ : Module S✝ M✝
r : R
S : S✝
M : RestrictScalars R S✝ M✝
⊢ (r • S) • M = r • S • M
[PROOFSTEP]
rw [Algebra.smul_def, mul_smul]
[GOAL]
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
inst✝⁴ : Semiring S✝
inst✝³ : AddCommMonoid M✝
inst✝² : CommSemiring R
inst✝¹ : Algebra R S✝
inst✝ : Module S✝ M✝
r : R
S : S✝
M : RestrictScalars R S✝ M✝
⊢ ↑(algebraMap R S✝) r • S • M = r • S • M
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ ↑(AddEquiv.symm (addEquiv R S M)) ((r • s) • x) = r • ↑(AddEquiv.symm (addEquiv R S M)) (s • x)
[PROOFSTEP]
rw [Algebra.smul_def, mul_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ ↑(AddEquiv.symm (addEquiv R S M)) (↑(algebraMap R S) r • s • x) = r • ↑(AddEquiv.symm (addEquiv R S M)) (s • x)
[PROOFSTEP]
rfl


[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
src✝¹ : Module R (A × B) := instModule
src✝ : R →+* A × B := RingHom.prod (algebraMap R A) (algebraMap R B)
⊢ ∀ (r : R) (x : (fun x => A × B) r),
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x =
      x *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r
[PROOFSTEP]
rintro r ⟨a, b⟩
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
src✝¹ : Module R (A × B) := instModule
src✝ : R →+* A × B := RingHom.prod (algebraMap R A) (algebraMap R B)
r : R
a : A
b : B
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      (a, b) =
    (a, b) *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r
[PROOFSTEP]
dsimp
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
src✝¹ : Module R (A × B) := instModule
src✝ : R →+* A × B := RingHom.prod (algebraMap R A) (algebraMap R B)
r : R
a : A
b : B
⊢ (↑(algebraMap R A) r * a, ↑(algebraMap R B) r * b) = (a * ↑(algebraMap R A) r, b * ↑(algebraMap R B) r)
[PROOFSTEP]
rw [commutes r a, commutes r b]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
src✝¹ : Module R (A × B) := instModule
src✝ : R →+* A × B := RingHom.prod (algebraMap R A) (algebraMap R B)
⊢ ∀ (r : R) (x : (fun x => A × B) r),
    r • x =
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x
[PROOFSTEP]
rintro r ⟨a, b⟩
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
src✝¹ : Module R (A × B) := instModule
src✝ : R →+* A × B := RingHom.prod (algebraMap R A) (algebraMap R B)
r : R
a : A
b : B
⊢ r • (a, b) =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      (a, b)
[PROOFSTEP]
dsimp
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
src✝¹ : Module R (A × B) := instModule
src✝ : R →+* A × B := RingHom.prod (algebraMap R A) (algebraMap R B)
r : R
a : A
b : B
⊢ (r • a, r • b) = (↑(algebraMap R A) r * a, ↑(algebraMap R B) r * b)
[PROOFSTEP]
rw [Algebra.smul_def r a, Algebra.smul_def r b]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
src✝ : A →+* B × C := RingHom.prod ↑f ↑g
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : A), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R A) r) =
    ↑(algebraMap R (B × C)) r
[PROOFSTEP]
simp only [toRingHom_eq_coe, RingHom.toFun_eq_coe, RingHom.prod_apply, coe_toRingHom, commutes, Prod.algebraMap_apply]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ comp (fst R B C) (prod f g) = f
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ↑(comp (fst R B C) (prod f g)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ comp (snd R B C) (prod f g) = g
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ↑(comp (snd R B C) (prod f g)) x✝ = ↑g x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : (A →ₐ[R] B) × (A →ₐ[R] C)
⊢ (fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f) = f
[PROOFSTEP]
ext
[GOAL]
case h₁.H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : (A →ₐ[R] B) × (A →ₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).fst x✝ = ↑f.fst x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂.H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : (A →ₐ[R] B) × (A →ₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).snd x✝ = ↑f.snd x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B × C
⊢ (fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f) = f
[PROOFSTEP]
ext
[GOAL]
case H.h₁
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).fst = (↑f x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case H.h₂
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).snd = (↑f x✝).snd
[PROOFSTEP]
rfl