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

eq_id_of_map_two_eq_two

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)

 871theorem eq_id_of_map_two_eq_two (f : JAut) (h2 : f posTwo = posTwo) : f = id := by

proof body

Tactic-mode proof.

 872  apply JAut.ext
 873  intro x
 874  rcases eq_self_or_inv f x with hfx | hfx
 875  · exact hfx
 876  · have hmul : f (posMul posTwo x) = posMul posTwo (posInv x) := by
 877      calc
 878        f (posMul posTwo x) = posMul (f posTwo) (f x) := f.multiplicative posTwo x
 879        _ = posMul posTwo (posInv x) := by rw [h2, hfx]
 880    rcases eq_self_or_inv f (posMul posTwo x) with htx | htx
 881    · have hx1 : x = posOne := (two_mul_inv_eq_two_mul_iff x).mp (hmul.symm.trans htx)
 882      subst x
 883      simpa [id] using hfx
 884    · exact False.elim ((two_mul_inv_ne_inv_two_mul x) (hmul.symm.trans htx))
 885
 886/-- The reciprocal automorphism is genuinely nontrivial. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.