help to prove roots = {a,b} (a = b)

Stream: new members

[Alex]

How to prove when A 0 0 = A 1 1? Thank you very much!

import Mathlib

variable {n : Type*} [DecidableEq n] [Fintype n]

variable {R : Type v} {M : Type w} [Field R]

variable [AddCommGroup M] [Module R M]

open Matrix Polynomial Module

noncomputable def det_charmatrix2x2_charpoly (A : Matrix (Fin 2) (Fin 2) R): R[X] :=  X^2 -(C (A 0 0) + C (A 1 1)) * X + C (A 0 0) * C (A 1 1) - C (A 0 1) * C (A 1 0)

lemma det_charmatrix2x2_charpoly_apply (A : Matrix (Fin 2) (Fin 2) R) : A.charmatrix.det = det_charmatrix2x2_charpoly A  :=by

  unfold charmatrix

  unfold det_charmatrix2x2_charpoly

  simp [Matrix.det_fin_two]

  rw [sub_mul,mul_sub,← pow_two,mul_sub,sub_sub,sub_add]

  congr 1

  rw [add_sub,mul_comm,← add_mul,add_comm]

lemma roots_char_trimatrix2x2 (A : Matrix (Fin 2) (Fin 2) R) (hA : A 0 1 = 0 ∨ A 1 0 = 0) (hA' : A 0 0 ≠ 0 ∧ A 1 1 ≠ 0):(det_charmatrix2x2_charpoly A).roots = {A 0 0, A 1 1}  := by

  have isroot :(det_charmatrix2x2_charpoly A).IsRoot (A 0 0) ∧ (det_charmatrix2x2_charpoly A).IsRoot (A 1 1) := by{

  rw [det_charmatrix2x2_charpoly]

  rcases hA with (h1 | h2)

  -- A 0 1 = 0

  · {

    simp [h1,zero_mul]

    split_ands

    repeat simp [add_mul,sub_add,← add_sub,mul_comm (A 1 1) (A 0 0),pow_two]

    }

  · {

    simp [h2,mul_zero]

    split_ands

    repeat simp [add_mul,sub_add,← add_sub,mul_comm (A 1 1) (A 0 0),pow_two]

    }

  }

  symm

  have hp0 : det_charmatrix2x2_charpoly A ≠ 0 := by

    rw [det_charmatrix2x2_charpoly]

    apply_fun (·.coeff 2)

    simp

  by_cases h : (A 0 0) ≠ (A 1 1)

  · {

    refine Multiset.eq_of_le_of_card_le ?_ ?_

    · rw [Multiset.le_iff_subset (by simp [h])]

      intro a ha

      simp? at ha says simp only [Multiset.insert_eq_cons, Multiset.mem_cons, Multiset.mem_singleton] at ha

      obtain rfl | rfl := ha

      · simpa [hp0] using isroot.1

      · simpa [hp0] using isroot.2

    · rw [Multiset.insert_eq_cons, Multiset.card_cons, Multiset.card_singleton]

      suffices h : (det_charmatrix2x2_charpoly A).natDegree = 1 + 1 from h ▸ (det_charmatrix2x2_charpoly A).card_roots'

      rw [det_charmatrix2x2_charpoly]

      compute_degree!

  }

  · {

    simp at h

    simp [h]

    sorry -- A 1 1 ::ₘ {A 1 1} = (det_charmatrix2x2_charpoly A).roots

    }