pith. machine review for the scientific record. sign in
theorem proved term proof

toList_injective

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  57theorem toList_injective {a b : LeptonMassRatios} (h : a.toList = b.toList) : a = b := by

proof body

Term-mode proof.

  58  simp only [toList] at h
  59  have h1 : a.mu_over_e = b.mu_over_e := List.cons.inj h |>.1
  60  have h23 := List.cons.inj h |>.2
  61  have h2 : a.tau_over_e = b.tau_over_e := List.cons.inj h23 |>.1
  62  have h3 : a.tau_over_mu = b.tau_over_mu := List.cons.inj (List.cons.inj h23 |>.2) |>.1
  63  exact ext h1 h2 h3
  64

depends on (4)

Lean names referenced from this declaration's body.