Lean defs to simplify some proving, I guess...

simps.lean

inductive sigmaprop (T:Type _)(P:T -> Prop) : Type _
| mksprop : (t:T) -> P t -> sigmaprop T P

def iscontr : Type _ -> Type _ := fun T => sigmaprop T (fun cc => (i:T) -> i = cc)

notation "~(" L "," R ")" => ⟨ L , R ⟩

def min_ps {P:T->Prop} : iscontr T -> (∀ i , P i) = (∃ i , P i) := by
  intro cp
  let (.mksprop cc cp) := cp
  let to : ((i:T) -> P i) -> (∃ i , P i) := fun f => ~( cc , f cc )
  let from_ : (∃ i , P i) -> (i:T) -> P i := fun ~( v2 , p ) k => by
    let eq : v2 = cc := cp v2
    let eq1 : k = cc := cp k
    let eq2 : k = v2 := by
      rw [eq]
      rw [eq1]
    rw [eq2]
    exact p
  exact Eq.propIntro to from_

def cntr_funsp : iscontr T -> iscontr (T -> T) := by
  intro cp
  let (.mksprop cc cp) := cp
  unfold iscontr
  exact (.mksprop id fun f => by
    funext k
    rw [cp k]
    simp
    generalize (f cc) = v
    rw [cp v]
  )

def no_autos : iscontr T -> {f : T -> T} -> f = id := by
  intros cp f
  let (.mksprop cc cf) := cp
  let ex : ∃ (f : T -> T) , f cc = cc := ~(id , by simp)
  funext k
  rw [cf k]
  simp
  let ac : ∀ (f : T -> T) , f cc = cc := by
    rw [min_ps (cntr_funsp cp)]
    exact ex
  exact (ac _)