[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
⊢ vandermonde (Fin.cons v0 v) = Fin.cons (fun j => v0 ^ ↑j) fun i => Fin.cons 1 fun j => v i * vandermonde v i j
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) i j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i j
[PROOFSTEP]
refine' Fin.cases (by simp) (fun i => _) i
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) 0 j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) 0 j
[PROOFSTEP]
simp
[GOAL]
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) j
[PROOFSTEP]
refine' Fin.cases (by simp) (fun j => _) j
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) 0 =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) 0
[PROOFSTEP]
simp
[GOAL]
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j✝ : Fin (n + 1)
i j : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) (Fin.succ j) =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) (Fin.succ j)
[PROOFSTEP]
simp [pow_succ]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin (Nat.succ n) → R
⊢ vandermonde v =
    Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v (Fin.succ i) * vandermonde (Fin.tail v) i j
[PROOFSTEP]
conv_lhs => rw [← Fin.cons_self_tail v, vandermonde_cons]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin (Nat.succ n) → R
| vandermonde v
[PROOFSTEP]
rw [← Fin.cons_self_tail v, vandermonde_cons]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin (Nat.succ n) → R
| vandermonde v
[PROOFSTEP]
rw [← Fin.cons_self_tail v, vandermonde_cons]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin (Nat.succ n) → R
| vandermonde v
[PROOFSTEP]
rw [← Fin.cons_self_tail v, vandermonde_cons]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
i j : Fin n
⊢ (vandermonde v * (vandermonde w)ᵀ) i j = ∑ k : Fin n, (v i * w j) ^ ↑k
[PROOFSTEP]
simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, mul_pow]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
i j : Fin n
⊢ ((vandermonde v)ᵀ * vandermonde v) i j = ∑ k : Fin n, v k ^ (↑i + ↑j)
[PROOFSTEP]
simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, pow_add]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
[PROOFSTEP]
unfold vandermonde
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
v : Fin Nat.zero → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin Nat.zero, ∏ j in Ioi i, (v j - v i)
[PROOFSTEP]
exact det_eq_one_of_card_eq_zero (Fintype.card_fin 0)
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n), ∏ j in Ioi i, (v j - v i)
[PROOFSTEP]
calc
  det (of fun i j : Fin n.succ => v i ^ (j : ℕ)) =
      det
        (of fun i j : Fin n.succ =>
          Matrix.vecCons (v 0 ^ (j : ℕ)) (fun i => v (Fin.succ i) ^ (j : ℕ) - v 0 ^ (j : ℕ)) i) :=
    det_eq_of_forall_row_eq_smul_add_const (Matrix.vecCons 0 1) 0 (Fin.cons_zero _ _) ?_
  _ =
      det
        (of fun i j : Fin n =>
          Matrix.vecCons (v 0 ^ (j.succ : ℕ)) (fun i : Fin n => v (Fin.succ i) ^ (j.succ : ℕ) - v 0 ^ (j.succ : ℕ))
            (Fin.succAbove 0 i)) :=
    by
    simp_rw [det_succ_column_zero, Fin.sum_univ_succ, of_apply, Matrix.cons_val_zero, submatrix, of_apply,
      Matrix.cons_val_succ, Fin.val_zero, pow_zero, one_mul, sub_self, mul_zero, zero_mul, Finset.sum_const_zero,
      add_zero]
  _ =
      det
        (of fun i j : Fin n =>
            (v (Fin.succ i) - v 0) * ∑ k in Finset.range (j + 1 : ℕ), v i.succ ^ k * v 0 ^ (j - k : ℕ) :
          Matrix _ _ R) :=
    by
    congr
    ext i j
    rw [Fin.succAbove_zero, Matrix.cons_val_succ, Fin.val_succ, mul_comm]
    exact (geom_sum₂_mul (v i.succ) (v 0) (j + 1 : ℕ)).symm
  _ =
      (Finset.prod Finset.univ (fun i => v (Fin.succ i) - v 0)) *
        det fun i j : Fin n => ∑ k in Finset.range (j + 1 : ℕ), v i.succ ^ k * v 0 ^ (j - k : ℕ) :=
    (det_mul_column (fun i => v (Fin.succ i) - v 0) _)
  _ = (Finset.prod Finset.univ (fun i => v (Fin.succ i) - v 0)) * det fun i j : Fin n => v (Fin.succ i) ^ (j : ℕ) :=
    (congr_arg _ ?_)
  _ = ∏ i : Fin n.succ, Finset.prod (Ioi i) (fun j => v j - v i) :=
    by
    simp_rw [Fin.prod_univ_succ, Fin.prod_Ioi_zero, Fin.prod_Ioi_succ]
    have h := ih (v ∘ Fin.succ)
    unfold Function.comp at h
    rw [h]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ det (↑of fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) =
    det
      (↑of fun i j =>
        vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j))
          (Fin.succAbove 0 i))
[PROOFSTEP]
simp_rw [det_succ_column_zero, Fin.sum_univ_succ, of_apply, Matrix.cons_val_zero, submatrix, of_apply,
  Matrix.cons_val_succ, Fin.val_zero, pow_zero, one_mul, sub_self, mul_zero, zero_mul, Finset.sum_const_zero, add_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ det
      (↑of fun i j =>
        vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j))
          (Fin.succAbove 0 i)) =
    det (↑of fun i j => (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k))
[PROOFSTEP]
congr
[GOAL]
case e_M.h.e_6.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (fun i j =>
      vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j))
        (Fin.succAbove 0 i)) =
    fun i j => (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)
[PROOFSTEP]
ext i j
[GOAL]
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin n
⊢ vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j)) (Fin.succAbove 0 i) =
    (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)
[PROOFSTEP]
rw [Fin.succAbove_zero, Matrix.cons_val_succ, Fin.val_succ, mul_comm]
[GOAL]
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin n
⊢ v (Fin.succ i) ^ (↑j + 1) - v 0 ^ (↑j + 1) =
    (∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) * (v (Fin.succ i) - v 0)
[PROOFSTEP]
exact (geom_sum₂_mul (v i.succ) (v 0) (j + 1 : ℕ)).symm
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    ∏ i : Fin (Nat.succ n), ∏ j in Ioi i, (v j - v i)
[PROOFSTEP]
simp_rw [Fin.prod_univ_succ, Fin.prod_Ioi_zero, Fin.prod_Ioi_succ]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
[PROOFSTEP]
have h := ih (v ∘ Fin.succ)
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
h : (det fun i j => (v ∘ Fin.succ) i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, ((v ∘ Fin.succ) j - (v ∘ Fin.succ) i)
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
[PROOFSTEP]
unfold Function.comp at h
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
h : (det fun i j => v (Fin.succ i) ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v (Fin.succ j) - v (Fin.succ i))
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
[PROOFSTEP]
rw [h]
[GOAL]
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ∀ (i j : Fin (Nat.succ n)),
    ↑of (fun i j => v i ^ ↑j) i j =
      ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) i j +
        vecCons 0 1 i * ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) 0 j
[PROOFSTEP]
intro i j
[GOAL]
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ ↑of (fun i j => v i ^ ↑j) i j =
    ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) i j +
      vecCons 0 1 i * ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) 0 j
[PROOFSTEP]
simp_rw [of_apply]
[GOAL]
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v i ^ ↑j =
    vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i +
      vecCons 0 1 i * vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) 0
[PROOFSTEP]
rw [Matrix.cons_val_zero]
[GOAL]
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v i ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i + vecCons 0 1 i * v 0 ^ ↑j
[PROOFSTEP]
refine' Fin.cases _ (fun i => _) i
[GOAL]
case succ.calc_1.refine'_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v 0 ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) 0 + vecCons 0 1 0 * v 0 ^ ↑j
[PROOFSTEP]
simp
[GOAL]
case succ.calc_1.refine'_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ v (Fin.succ i) ^ ↑j =
    vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) (Fin.succ i) + vecCons 0 1 (Fin.succ i) * v 0 ^ ↑j
[PROOFSTEP]
rw [Matrix.cons_val_succ, Matrix.cons_val_succ, Pi.one_apply]
[GOAL]
case succ.calc_1.refine'_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ v (Fin.succ i) ^ ↑j = v (Fin.succ i) ^ ↑j - v 0 ^ ↑j + 1 * v 0 ^ ↑j
[PROOFSTEP]
ring
[GOAL]
case succ.calc_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
[PROOFSTEP]
cases n
[GOAL]
case succ.calc_2.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
ih : ∀ (v : Fin Nat.zero → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin Nat.zero, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ Nat.zero) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
[PROOFSTEP]
rw [det_eq_one_of_card_eq_zero (Fintype.card_fin 0), det_eq_one_of_card_eq_zero (Fintype.card_fin 0)]
[GOAL]
case succ.calc_2.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
[PROOFSTEP]
apply det_eq_of_forall_col_eq_smul_add_pred fun _ => v 0
[GOAL]
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ ∀ (i : Fin (n✝ + 1)), ∑ k in range (↑0 + 1), v (Fin.succ i) ^ k * v 0 ^ (↑0 - k) = v (Fin.succ i) ^ ↑0
[PROOFSTEP]
intro j
[GOAL]
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
j : Fin (n✝ + 1)
⊢ ∑ k in range (↑0 + 1), v (Fin.succ j) ^ k * v 0 ^ (↑0 - k) = v (Fin.succ j) ^ ↑0
[PROOFSTEP]
simp
[GOAL]
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ ∀ (i : Fin (n✝ + 1)) (j : Fin n✝),
    ∑ k in range (↑(Fin.succ j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.succ j) - k) =
      v (Fin.succ i) ^ ↑(Fin.succ j) +
        v 0 * ∑ k in range (↑(Fin.castSucc j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.castSucc j) - k)
[PROOFSTEP]
intro i j
[GOAL]
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ k in range (↑(Fin.succ j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.succ j) - k) =
    v (Fin.succ i) ^ ↑(Fin.succ j) +
      v 0 * ∑ k in range (↑(Fin.castSucc j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.castSucc j) - k)
[PROOFSTEP]
simp only [smul_eq_mul, Pi.add_apply, Fin.val_succ, Fin.coe_castSucc, Pi.smul_apply]
[GOAL]
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ x in range (↑j + 1 + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    v (Fin.succ i) ^ (↑j + 1) + v 0 * ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j - x)
[PROOFSTEP]
rw [Finset.sum_range_succ, add_comm, tsub_self, pow_zero, mul_one, Finset.mul_sum]
[GOAL]
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ v (Fin.succ i) ^ (↑j + 1) + ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    v (Fin.succ i) ^ (↑j + 1) + ∑ x in range (↑j + 1), v 0 * (v (Fin.succ i) ^ x * v 0 ^ (↑j - x))
[PROOFSTEP]
congr 1
[GOAL]
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    ∑ x in range (↑j + 1), v 0 * (v (Fin.succ i) ^ x * v 0 ^ (↑j - x))
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i' hi' => _
[GOAL]
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ v (Fin.succ i) ^ i' * v 0 ^ (↑j + 1 - i') = v 0 * (v (Fin.succ i) ^ i' * v 0 ^ (↑j - i'))
[PROOFSTEP]
rw [mul_left_comm (v 0), Nat.succ_sub, pow_succ]
[GOAL]
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ i' ≤ ↑j
[PROOFSTEP]
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp hi')
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) = 0 ↔ ∃ i j, v i = v j ∧ i ≠ j
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) = 0 → ∃ i j, v i = v j ∧ i ≠ j
[PROOFSTEP]
simp only [det_vandermonde v, Finset.prod_eq_zero_iff, sub_eq_zero, forall_exists_index]
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x : Fin n), (x ∈ univ ∧ ∃ a, a ∈ Ioi x ∧ v a = v x) → ∃ i j, v i = v j ∧ i ≠ j
[PROOFSTEP]
rintro i ⟨_, j, h₁, h₂⟩
[GOAL]
case mp.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i : Fin n
left✝ : i ∈ univ
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ i j, v i = v j ∧ i ≠ j
[PROOFSTEP]
exact ⟨j, i, h₂, (mem_Ioi.mp h₁).ne'⟩
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → det (vandermonde v) = 0
[PROOFSTEP]
simp only [Ne.def, forall_exists_index, and_imp]
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → det (vandermonde v) = 0
[PROOFSTEP]
refine' fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => _)
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ vandermonde v i k = vandermonde v j k
[PROOFSTEP]
rw [vandermonde_apply, vandermonde_apply, h₁]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) ≠ 0 ↔ Function.Injective v
[PROOFSTEP]
unfold Function.Injective
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) ≠ 0 ↔ ∀ ⦃a₁ a₂ : Fin n⦄, v a₁ = v a₂ → a₁ = a₂
[PROOFSTEP]
simp only [det_vandermonde_eq_zero_iff, Ne.def, not_exists, not_and, Classical.not_not]
[GOAL]
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ v = 0
[PROOFSTEP]
apply eq_zero_of_forall_index_sum_pow_mul_eq_zero hf
[GOAL]
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ ∀ (j : Fin n), ∑ i : Fin n, f j ^ ↑i * v i = 0
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ ∀ (j : Fin n), ∑ x : Fin n, v x * f j ^ ↑x = 0
[PROOFSTEP]
exact hfv


[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_4
⊢ map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)
[PROOFSTEP]
rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
⊢ 1 ≠ AddMonoid.toZero.1
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : IsEmpty ι
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ ↑(map ι f) x = x
[PROOFSTEP]
induction' x using Module.Ray.ind with g hg
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ ↑(map ι f) (rayOfNeZero R g hg) = rayOfNeZero R g hg
[PROOFSTEP]
rw [Orientation.map_apply]
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ rayOfNeZero R (AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f))
      (_ : ¬AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f) = 0) =
    rayOfNeZero R g hg
[PROOFSTEP]
congr
[GOAL]
case h.e_v
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f) = g
[PROOFSTEP]
ext i
[GOAL]
case h.e_v.H
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ ↑(AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f)) i = ↑g i
[PROOFSTEP]
rw [AlternatingMap.compLinearMap_apply]
[GOAL]
case h.e_v.H
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ (↑g fun i_1 => ↑↑(LinearEquiv.symm f) (i i_1)) = ↑g i
[PROOFSTEP]
congr
[GOAL]
case h.e_v.H.h.e_6.h
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ (fun i_1 => ↑↑(LinearEquiv.symm f) (i i_1)) = i
[PROOFSTEP]
simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
case intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
[PROOFSTEP]
induction' x using Module.Ray.ind with g hg
[GOAL]
case intro.h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ ↑(Orientation.map ι f) (rayOfNeZero R g hg) = (↑LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg
[PROOFSTEP]
rw [Orientation.map_apply, smul_rayOfNeZero, ray_eq_iff, Units.smul_def, (g.compLinearMap f.symm).eq_smul_basis_det e,
  g.eq_smul_basis_det e, AlternatingMap.compLinearMap_apply, AlternatingMap.smul_apply,
  show (fun i ↦ (LinearEquiv.symm f).toLinearMap (e i)) = (LinearEquiv.symm f).toLinearMap ∘ e by rfl, Basis.det_comp,
  Basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul, LinearEquiv.coe_inv_det]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ (fun i => ↑↑(LinearEquiv.symm f) (↑e i)) = ↑↑(LinearEquiv.symm f) ∘ ↑e
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
f : M ≃ₗ[R] N
⊢ Basis.orientation (Basis.map e f) = ↑(Orientation.map ι f) (Basis.orientation e)
[PROOFSTEP]
simp_rw [Basis.orientation, Orientation.map_apply, Basis.det_map']
[GOAL]
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
w : ι → Rˣ
⊢ Basis.orientation (unitsSMul e w) = (∏ i : ι, w i)⁻¹ • Basis.orientation e
[PROOFSTEP]
rw [Basis.orientation, Basis.orientation, smul_rayOfNeZero, ray_eq_iff, e.det.eq_smul_basis_det (e.unitsSMul w),
  det_unitsSMul_self, Units.smul_def, smul_smul]
[GOAL]
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) ((↑(∏ i : ι, w i)⁻¹ * ∏ i : ι, ↑(w i)) • det (unitsSMul e w))
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) (↑((∏ i : ι, w i)⁻¹ * ∏ i : ι, w i) • det (unitsSMul e w))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) (det (unitsSMul e w))
[PROOFSTEP]
exact SameRay.rfl
[GOAL]
R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ Basis.orientation b = positiveOrientation
[PROOFSTEP]
rw [Basis.orientation]
[GOAL]
R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ rayOfNeZero R (det b) (_ : det b ≠ 0) = positiveOrientation
[PROOFSTEP]
congr
[GOAL]
case e_v
R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ det b = ↑AlternatingMap.constLinearEquivOfIsEmpty 1
[PROOFSTEP]
exact b.det_isEmpty
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
o : Orientation R M ι
⊢ o = positiveOrientation ∨ o = -positiveOrientation
[PROOFSTEP]
induction' o using Module.Ray.ind with x hx
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx = positiveOrientation ∨ rayOfNeZero R x hx = -positiveOrientation
[PROOFSTEP]
dsimp [positiveOrientation]
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx =
      rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1)
        (_ :
          ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) ∨
    rayOfNeZero R x hx =
      rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) (_ : ¬-AlternatingMap.constOfIsEmpty R M ι 1 = 0)
[PROOFSTEP]
simp only [ray_eq_iff, sameRay_neg_swap]
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)
[PROOFSTEP]
rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ ¬LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
[PROOFSTEP]
intro h
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
⊢ False
[PROOFSTEP]
set f : AlternatingMap R M R ι ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ False
[PROOFSTEP]
have H : LinearIndependent R ![f x, 1] := by
  convert h.map' f.toLinearMap f.ker
  ext i
  fin_cases i <;> simp
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ LinearIndependent R ![↑f x, 1]
[PROOFSTEP]
convert h.map' f.toLinearMap f.ker
[GOAL]
case h.e'_4
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ ![↑f x, 1] = ↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]
[PROOFSTEP]
ext i
[GOAL]
case h.e'_4.h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
i : Fin (Nat.succ (Nat.succ 0))
⊢ Matrix.vecCons (↑f x) ![1] i = (↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.e'_4.h.head
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ Matrix.vecCons (↑f x) ![1] { val := 0, isLt := (_ : 0 < Nat.succ (Nat.succ 0)) } =
    (↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) { val := 0, isLt := (_ : 0 < Nat.succ (Nat.succ 0)) }
[PROOFSTEP]
simp
[GOAL]
case h.e'_4.h.tail.head
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ Matrix.vecCons (↑f x) ![1] { val := 1, isLt := (_ : (fun a => a < Nat.succ (Nat.succ 0)) 1) } =
    (↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1])
      { val := 1, isLt := (_ : (fun a => a < Nat.succ (Nat.succ 0)) 1) }
[PROOFSTEP]
simp
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H : LinearIndependent R ![↑f x, 1]
⊢ False
[PROOFSTEP]
rw [linearIndependent_iff'] at H
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ (Nat.succ 0)))) (g : Fin (Nat.succ (Nat.succ 0)) → R),
    ∑ i in s, g i • Matrix.vecCons (↑f x) ![1] i = 0 → ∀ (i : Fin (Nat.succ (Nat.succ 0))), i ∈ s → g i = 0
⊢ False
[PROOFSTEP]
simpa using H Finset.univ ![1, -f x] (by simp [Fin.sum_univ_succ]) 0 (by simp)
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ (Nat.succ 0)))) (g : Fin (Nat.succ (Nat.succ 0)) → R),
    ∑ i in s, g i • Matrix.vecCons (↑f x) ![1] i = 0 → ∀ (i : Fin (Nat.succ (Nat.succ 0))), i ∈ s → g i = 0
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons 1 ![-↑f x] i • Matrix.vecCons (↑f x) ![1] i = 0
[PROOFSTEP]
simp [Fin.sum_univ_succ]
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ (Nat.succ 0)))) (g : Fin (Nat.succ (Nat.succ 0)) → R),
    ∑ i in s, g i • Matrix.vecCons (↑f x) ![1] i = 0 → ∀ (i : Fin (Nat.succ (Nat.succ 0))), i ∈ s → g i = 0
⊢ 0 ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e₁ e₂ : Basis ι R M
⊢ SameRay R (det e₁) (det e₂) ↔ SameRay R (↑(det e₁) ↑e₂ • det e₂) (det e₂)
[PROOFSTEP]
rw [← e₁.det.eq_smul_basis_det e₂]
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : Orientation R M ι
⊢ x = Basis.orientation e ∨ x = -Basis.orientation e
[PROOFSTEP]
induction' x using Module.Ray.ind with x hx
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx = Basis.orientation e ∨ rayOfNeZero R x hx = -Basis.orientation e
[PROOFSTEP]
rw [← x.map_basis_ne_zero_iff e] at hx
[GOAL]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : AlternatingMap R M R ι
hx✝ : x ≠ 0
hx : ↑x ↑e ≠ 0
⊢ rayOfNeZero R x hx✝ = Basis.orientation e ∨ rayOfNeZero R x hx✝ = -Basis.orientation e
[PROOFSTEP]
rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
  sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx, lt_or_lt_iff_ne,
  ne_comm]
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ Basis.orientation (Basis.map e f) = Basis.orientation e ↔ 0 < ↑LinearMap.det ↑f
[PROOFSTEP]
rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff, LinearEquiv.coe_det]
[GOAL]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ Basis.orientation (Basis.map e f) = -Basis.orientation e ↔ ↑LinearMap.det ↑f < 0
[PROOFSTEP]
rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]
[GOAL]
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
i : ι
⊢ Basis.orientation (unitsSMul e (Function.update 1 i (-1))) = -Basis.orientation e
[PROOFSTEP]
rw [orientation_unitsSMul, Finset.prod_update_of_mem (Finset.mem_univ _)]
[GOAL]
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
i : ι
⊢ (-1 * ∏ x in Finset.univ \ {i}, OfNat.ofNat 1 x)⁻¹ • Basis.orientation e = -Basis.orientation e
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ Basis.orientation (adjustToOrientation e x) = x
[PROOFSTEP]
rw [adjustToOrientation]
[GOAL]
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ Basis.orientation
      (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) =
    x
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : Basis.orientation e = x
⊢ Basis.orientation e = x
[PROOFSTEP]
exact h
[GOAL]
case neg
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬Basis.orientation e = x
⊢ Basis.orientation (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = x
[PROOFSTEP]
rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]
[GOAL]
case neg
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬Basis.orientation e = x
⊢ Basis.orientation e ≠ x
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
⊢ ↑(adjustToOrientation e x) i = ↑e i ∨ ↑(adjustToOrientation e x) i = -↑e i
[PROOFSTEP]
rw [adjustToOrientation]
[GOAL]
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
⊢ ↑(if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : Basis.orientation e = x
⊢ ↑e i = ↑e i ∨ ↑e i = -↑e i
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : ¬Basis.orientation e = x
⊢ ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
[PROOFSTEP]
by_cases hi : i = Classical.arbitrary ι
[GOAL]
case pos
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : ¬Basis.orientation e = x
hi : i = Classical.arbitrary ι
⊢ ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
[PROOFSTEP]
simp [unitsSMul_apply, hi]
[GOAL]
case neg
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : ¬Basis.orientation e = x
hi : ¬i = Classical.arbitrary ι
⊢ ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
[PROOFSTEP]
simp [unitsSMul_apply, hi]
[GOAL]
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ det (adjustToOrientation e x) = det e ∨ det (adjustToOrientation e x) = -det e
[PROOFSTEP]
dsimp [Basis.adjustToOrientation]
[GOAL]
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ det (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = det e ∨
    det (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : Basis.orientation e = x
⊢ det e = det e ∨ det e = -det e
[PROOFSTEP]
left
[GOAL]
case pos.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : Basis.orientation e = x
⊢ det e = det e
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = det e ∨
    det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
[PROOFSTEP]
right
[GOAL]
case neg.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
[PROOFSTEP]
simp [e.det_unitsSMul, ← Units.coe_prod, Finset.prod_update_of_mem]
[GOAL]
case neg.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ -1 • det e = -det e
[PROOFSTEP]
ext
[GOAL]
case neg.h.H
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
x✝ : ι → M
⊢ ↑(-1 • det e) x✝ = ↑(-det e) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
v : ι → M
⊢ |↑(det (adjustToOrientation e x)) v| = |↑(det e) v|
[PROOFSTEP]
cases' e.det_adjustToOrientation x with h h
[GOAL]
case inl
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
v : ι → M
h : det (adjustToOrientation e x) = det e
⊢ |↑(det (adjustToOrientation e x)) v| = |↑(det e) v|
[PROOFSTEP]
simp [h]
[GOAL]
case inr
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_3
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
v : ι → M
h : det (adjustToOrientation e x) = -det e
⊢ |↑(det (adjustToOrientation e x)) v| = |↑(det e) v|
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
have e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
have orientation_neg_neg : ∀ f : Basis ι R M, - -Basis.orientation f = Basis.orientation f := by simp
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
rcases e.orientation_eq_or_eq_neg x₁ with (h₁ | h₁)
[GOAL]
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
h₁ : x₁ = Basis.orientation e
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)
[GOAL]
case inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
h₁ : x₁ = -Basis.orientation e
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)
[GOAL]
case inl.inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
h₁ : x₁ = Basis.orientation e
h₂ : x₂ = Basis.orientation e
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
simp [h₁, h₂, orientation_neg_neg]
[GOAL]
case inl.inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
h₁ : x₁ = Basis.orientation e
h₂ : x₂ = -Basis.orientation e
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
simp [h₁, h₂, orientation_neg_neg]
[GOAL]
case inr.inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
h₁ : x₁ = -Basis.orientation e
h₂ : x₂ = Basis.orientation e
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
simp [h₁, h₂, orientation_neg_neg]
[GOAL]
case inr.inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
h₁ : x₁ = -Basis.orientation e
h₂ : x₂ = -Basis.orientation e
⊢ x₁ = x₂ ∨ x₁ = -x₂
[PROOFSTEP]
simp [h₁, h₂, orientation_neg_neg]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
[PROOFSTEP]
have H : finrank R M = 0 := by
  refine' h.symm.trans _
  convert @Fintype.card_of_isEmpty ι _
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ finrank R M = 0
[PROOFSTEP]
refine' h.symm.trans _
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ Fintype.card ι = 0
[PROOFSTEP]
convert @Fintype.card_of_isEmpty ι _
[GOAL]
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
H : finrank R M = 0
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
[PROOFSTEP]
simp [LinearMap.det_eq_one_of_finrank_eq_zero H]
[GOAL]
case inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
[PROOFSTEP]
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_self_iff, LinearEquiv.coe_det]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
⊢ ↑(map ι f) x = -x ↔ ↑LinearMap.det ↑f < 0
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ ↑(map ι f) x = -x ↔ ↑LinearMap.det ↑f < 0
[PROOFSTEP]
have H : finrank R M = 0 := by
  refine' h.symm.trans _
  convert @Fintype.card_of_isEmpty ι _
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ finrank R M = 0
[PROOFSTEP]
refine' h.symm.trans _
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ Fintype.card ι = 0
[PROOFSTEP]
convert @Fintype.card_of_isEmpty ι _
[GOAL]
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
H : finrank R M = 0
⊢ ↑(map ι f) x = -x ↔ ↑LinearMap.det ↑f < 0
[PROOFSTEP]
simp [LinearMap.det_eq_one_of_finrank_eq_zero H, Module.Ray.ne_neg_self x]
[GOAL]
case inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ ↑(map ι f) x = -x ↔ ↑LinearMap.det ↑f < 0
[PROOFSTEP]
have H : 0 < finrank R M := by
  rw [← h]
  exact Fintype.card_pos
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < finrank R M
[PROOFSTEP]
rw [← h]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < Fintype.card ι
[PROOFSTEP]
exact Fintype.card_pos
[GOAL]
case inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
H : 0 < finrank R M
⊢ ↑(map ι f) x = -x ↔ ↑LinearMap.det ↑f < 0
[PROOFSTEP]
haveI : FiniteDimensional R M := finiteDimensional_of_finrank H
[GOAL]
case inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
H : 0 < finrank R M
this : FiniteDimensional R M
⊢ ↑(map ι f) x = -x ↔ ↑LinearMap.det ↑f < 0
[PROOFSTEP]
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]


[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ A * star A = 1
[PROOFSTEP]
refine' ⟨And.right, fun hA => ⟨_, hA⟩⟩
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A * star A = 1
⊢ star A * A = 1
[PROOFSTEP]
simpa only [mul_eq_one_comm] using hA
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ star A * A = 1
[PROOFSTEP]
refine' ⟨And.left, fun hA => ⟨hA, _⟩⟩
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : star A * A = 1
⊢ A * star A = 1
[PROOFSTEP]
rwa [mul_eq_one_comm] at hA
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ det A ∈ unitary α
[PROOFSTEP]
constructor
[GOAL]
case left
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ star (det A) * det A = 1
[PROOFSTEP]
simpa [star, det_transpose] using congr_arg det hA.1
[GOAL]
case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ det A * star (det A) = 1
[PROOFSTEP]
simpa [star, det_transpose] using congr_arg det hA.2
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(comp (toLin' A⁻¹) (toLin' A)) x = ↑(toLin' (A⁻¹ * A)) x
[PROOFSTEP]
rw [← toLin'_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(toLin' (A⁻¹ * A)) x = x
[PROOFSTEP]
rw [mul_left_inv, toLin'_one, id_apply]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(comp (toLin' A) (toLin' A⁻¹)) x = ↑(toLin' (A * A⁻¹)) x
[PROOFSTEP]
rw [← toLin'_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(toLin' (A * A⁻¹)) x = x
[PROOFSTEP]
rw [mul_right_inv, toLin'_one, id_apply]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ ↑(toGL 1) = ↑1
[PROOFSTEP]
simp only [coe_toGL, toLin'_one]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ LinearMap.id = ↑1
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A B : { x // x ∈ unitaryGroup n α }
⊢ ↑(toGL (A * B)) = ↑(toGL A * toGL B)
[PROOFSTEP]
simp only [coe_toGL, toLin'_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A B : { x // x ∈ unitaryGroup n α }
⊢ comp (toLin' A) (toLin' B) = ↑(toGL A * toGL B)
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
⊢ A ∈ orthogonalGroup n β ↔ A * star A = 1
[PROOFSTEP]
refine' ⟨And.right, fun hA => ⟨_, hA⟩⟩
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : A * star A = 1
⊢ star A * A = 1
[PROOFSTEP]
simpa only [mul_eq_one_comm] using hA
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
⊢ A ∈ orthogonalGroup n β ↔ star A * A = 1
[PROOFSTEP]
refine' ⟨And.left, fun hA => ⟨hA, _⟩⟩
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : star A * A = 1
⊢ A * star A = 1
[PROOFSTEP]
rwa [mul_eq_one_comm] at hA