[WIP] remove the (now) redundant hfunext

analysis/topology/infinite_sum.lean

@@ -15,6 +15,7 @@ import logic.function algebra.big_operators data.set data.finset
 noncomputable theory
 open set lattice finset filter function classical
 local attribute [instance] prop_decidable
+local attribute [-congr] pi_congr_eq
 
 variables {α : Type*} {β : Type*} {γ : Type*}
 

data/coinductive/basic.lean

@@ -417,7 +417,7 @@ begin
     { unfold head, rw [← h,head_succ' n _ x_approx x_consistent] },
     introv h',
     congr, rw h,
-    transitivity y, apply h',
+    transitivity a', apply h',
     symmetry, apply cast_heq, },
 end
 

data/pfun.lean

@@ -111,7 +111,7 @@ instance : is_lawful_monad roption :=
 
 instance : monad_fail roption :=
 { fail := λ_ _, roption.none, ..roption.monad }
-
+open function
 lemma assert_if_neg {p : Prop}
   (x : p → roption α)
   (h : ¬ p)
@@ -122,7 +122,7 @@ by { dsimp [assert,roption.none],
        exact h h' },
      congr,
      repeat { rw this <|> apply hfunext },
-     intros, cases y, }
+     intros h h', cases h', }
 
 lemma assert_if_pos {p : Prop}
   (x : p → roption α)

data/set/countable.lean

@@ -137,9 +137,6 @@ have {t | finite t ∧ t ⊆ s } ⊆
           set.ext $ assume x,
           begin
             simp [eq.symm, iff_def, or_imp_distrib, has] {contextual:=tt},
-            constructor,
-            exact assume hxs, or.imp_right (assume hxt', ⟨hxs, hxt'⟩),
-            exact assume hxs hxt', ⟨hxs, or.inr hxt'⟩,
           end⟩ }
   end,
 by haveI enc := h.to_encodable; exact

logic/basic.lean

@@ -607,25 +607,6 @@ iff.intro (assume ⟨f⟩ a, ⟨f a⟩) (assume f, ⟨assume a, classical.choice
 
 end nonempty
 
-section hfunext
-universes u v
-variables {α : Sort u} {β : Sort u} {γ : Sort v}
-
-variables (f : α → γ) (g : β → γ)
-variables h₀ : α = β
-variables h₁ : ∀ (x : α) (y : β), x == y → f x = g y
-include h₀ h₁
-lemma hfunext : f == g :=
-begin
-  subst β,
-  apply heq_of_eq,
-  apply funext, intro i,
-  apply h₁,
-  refl,
-end
-
-end hfunext
-
 @[congr]
 lemma pi_congr_eq {a : Sort*} {p q : a → Sort*} (h : ∀ x, p x = q x)
 : (Π x, p x) = Π x, q x :=