gistfile1.lean

def heq_from (eq1:A=B)(k1:@HEq A a A (by subst eq1; exact b)): @HEq A a B b := by
  simp only [heq_eq_eq] at k1
  rw [@eqRec_eq_cast] at k1
  cases eq1
  simp only [cast_eq] at k1
  rw [<-heq_eq_eq] at k1
  exact k1

def heq_heq (eq1:A=B): (@HEq A a A (by subst eq1; exact b)) = (@HEq A a B b) := by
  apply propext
  apply Iff.intro
  exact heq_from eq1
  intro i
  cases eq1
  simp only [heq_eq_eq]
  rw [heq_eq_eq] at i
  exact i

def subtype_val_eq {f:A->Prop}{p1:f a1}{p2:f a2}(p1:(Subtype.mk a1 p1) = (Subtype.mk a2 p2)): a1 = a2 := by
  cases p1
  rfl

set_option pp.proofs true in
def unstuck_rec {A: Type _}{B:Type _}(eq:Eq A B){val:B}
: (@Eq.rec Type
    A (fun x _ => {_ : x} → A) (fun {b} => b) B
    eq
    val) = (by rw [eq]; exact val)
:= by
  cases eq
  rfl

-- def __eww (k:a=b): a=b := by
--   cases k
--   exact __eww (Eq.refl _)

mutual

-- set_option pp.proofs true in
-- set_option pp.parens true in
-- set_option pp.fieldNotation false in
def reduce_cast_subtype_proj_1_ {A : Type}{p1 p2 : A → Prop}{k:{i // p1 i}} (eq : {i // p1 i} = {i // p2 i}):
  (cast eq k).val = k.val
:= by
  let eq0 : ({ i // (p2 i) } → A) = ({ i // (p1 i) } → A) := implies_congr (Eq.symm eq) rfl
  apply congr_heq
  {
    refine heq_of_eqRec_eq ?_ ?_
    exact eq0
    rw [@eqRec_eq_cast]
    generalize eq1 : (implies_congr (Eq.symm eq) rfl) = k
    -- let eq3 
    -- : HEq (@Eq.rec Type ({ i // (p2 i) } → A) (fun x h => (({ i // (p2 i) } → A) = x)) rfl ({ i // (p1 i) } → A) k) 
    --       (@rfl Type ({ i // (p2 i) } → A)) 
    -- := by
    --   exact (eqRec_heq k rfl)
    -- let eq4 : 
    --   (@Eq.rec Type ({ i // (p2 i) } → A) (fun x h => (({ i // (p2 i) } → A) = x)) rfl ({ i // (p1 i) } → A) k)
    --   = 
    --   (by rewrite [eq0]; rfl)
    -- := by
    --   exact eq1
    -- -- dsimp at eq4
    -- rw [eq4]
    -- rw [(cast_eq rfl k)]
    -- let eq5 : (@Subtype.val A fun i => (p1 i)) = cast rfl (@Subtype.val A fun i => (p1 i)) := by rfl
    -- rw [eq5]
    -- let eq7 : HEq k (@rfl Type ({ i // (p1 i) } → A)) := by
    --   exact (heq_of_eqRec_eq (congrFun (congrArg Eq eq0) ({ i // (p1 i) } → A)) rfl)
    let eq8 : (@Subtype.val A fun i => (p2 i)) = (by rw [<-eq]; exact @Subtype.val A fun i => (p1 i)) := by
      dsimp only [eq_mpr_eq_cast]
      refine (Iff.mpr eq_cast_iff_heq ?_)
      -- fun cast irrel
      refine (Function.hfunext (id (Eq.symm eq)) ?_)
      intro (.mk i2 p7) (.mk i3 p8) eq9
      refine (heq_of_eq ?_)
      dsimp
      apply heq_subtype_to_eq_val
      exact eq9
    simp at eq8
    rw [eq8]
    simp only [cast_cast, cast_eq]
  }
  exact cast_heq eq k

-- set_option pp.proofs true in
def heq_subtype_to_eq_val
  {A:Type}{n1 n2:A}
  {p1 p2:A->Prop}{k1: p1 n1}{k2: p2 n2}
  (eq: @HEq { i // p1 i } ⟨n1, k1⟩ { i // p2 i } ⟨n2, k2⟩)
: n1 = n2
:= by
  let t_eq := type_eq_of_heq eq
  rw [<- (heq_heq t_eq)] at eq
  simp only [heq_eq_eq] at eq
  let eq3 := subtype_val_eq eq
  rw [unstuck_rec] at eq3
  simp only [eq_mpr_eq_cast] at eq3
  rw [eq3]
  apply reduce_cast_subtype_proj_1_

end