§ Leibniz Equality in Lean4

@[simp, reducible]
abbrev Leibniz {A: Type} (x y: A) := ∀ (P: A -> Prop), P x -> P y

theorem Leibniz_refl {A: Type}: ∀ (x: A), Leibniz x x := fun _A _P Px => Px
theorem Leibniz_trans {A: Type}: ∀ (x y z: A), Leibniz x y -> Leibniz y z  -> Leibniz x z :=
        fun _x _y _z Lxy Lyz P Px => Lyz P (Lxy P Px)

theorem Leibniz_sym {A: Type}: ∀ (x y: A), Leibniz x y -> Leibniz y x :=
  fun x y  Lxy P Py =>
      let prop (a: A) := P a -> P x
      let proofPropX : prop x := id
      let proofPropY: prop y := Lxy prop proofPropX
      proofPropY Py

theorem defeq_implies_Leibniz (x y: A) (EQ: x = y):
  Leibniz x y := fun P Px => EQ ▸ Px

theorem Leibniz_implies_defeq (x y: A) (LEQ: Leibniz x y):
  x = y := LEQ (fun a => x = a) rfl