feat: use to_dual for HeytingAlgebra (leanprover-community#33543)

This PR adds `to_dual` for `HeytingAlgebra`, `BiheytingAlgebra`, `GeneralizedHeytingAlgebra`.

There is a bit of friction around dualizing `compl` to `hnot`, because this means that theorems about `compl` in boolean algebras will not be able to be translated nicely with `to_dual`. This should not be that many theorems, so this is acceptable.

See also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Dualize.20sdiff.20and.20himp/with/599261487

Since we have `GeneralizedCoheytingAlgebra.toDistribLattice`, I removed `CoheytingAlgebra.toDistribLattice`.

Aligning the `Heyting` and `Coheyting` API is kind of awkward, because they are unfortunately quite different. One reason is that the arguments of `sup`/`inf` are often swapped in the dual version, which is not compatible with `to_dual`. I've worked around this with extensive use of `to_dual none`.

There are quite some lemmas that in my eyes seem unnecessary, such as `le_sup_sdiff_sup_sdiff`, but I haven't removed any in this PR.

Author: JovanGerb

Mathlib/Combinatorics/SetFamily/Kleitman.lean

@@ -64,7 +64,7 @@ theorem Finset.card_biUnion_le_of_intersecting (s : Finset ι) (f : ι → Finse
   refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
   nth_rw 1 [cons_eq_insert i]
   rw [biUnion_insert]
-  refine (card_mono <| @le_sup_sdiff _ _ _ <| f' i).trans ((card_union_le _ _).trans ?_)
+  refine (card_mono <| @le_sup_sdiff _ _ (f' i) _).trans ((card_union_le _ _).trans ?_)
   rw [union_sdiff_left, sdiff_eq_inter_compl]
   refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
   rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]

Mathlib/Data/Finset/Lattice/Fold.lean

@@ -407,10 +407,14 @@ theorem sup_himp_left (hs : s.Nonempty) (f : ι → α) (a : α) :
     (s.sup fun b => a ⇨ f b) = a ⇨ s.sup f :=
   @inf_sdiff_right αᵒᵈ _ _ _ hs _ _
 
-@[to_dual (attr := simp)]
+@[simp]
 protected theorem compl_sup (s : Finset ι) (f : ι → α) : (s.sup f)ᶜ = s.inf fun i => (f i)ᶜ :=
   map_finset_sup (OrderIso.compl α) _ _
 
+@[simp]
+protected theorem compl_inf (s : Finset ι) (f : ι → α) : (s.inf f)ᶜ = s.sup fun i => (f i)ᶜ :=
+  map_finset_inf (OrderIso.compl α) _ _
+
 end BooleanAlgebra
 
 section LinearOrder

Mathlib/Order/Basic.lean

@@ -522,15 +522,16 @@ lemma LinearOrder.ext_lt {A B : LinearOrder α} (H : ∀ x y : α, (haveI := A;
 instance Prop.instCompl : Compl Prop :=
   ⟨Not⟩
 
+@[to_dual instHNot]
 instance Pi.instCompl [∀ i, Compl (π i)] : Compl (∀ i, π i) :=
   ⟨fun x i ↦ (x i)ᶜ⟩
 
-@[push ←]
+@[to_dual (attr := push ←) hnot_def]
 theorem Pi.compl_def [∀ i, Compl (π i)] (x : ∀ i, π i) :
     xᶜ = fun i ↦ (x i)ᶜ :=
   rfl
 
-@[simp]
+@[to_dual (attr := simp) hnot_apply]
 theorem Pi.compl_apply [∀ i, Compl (π i)] (x : ∀ i, π i) (i : ι) :
     xᶜ i = (x i)ᶜ :=
   rfl
@@ -647,15 +648,16 @@ theorem lt_update_self_iff : x < update x i a ↔ x i < a := by simp [lt_iff_le_
 
 end Function
 
-instance Pi.sdiff [∀ i, SDiff (π i)] : SDiff (∀ i, π i) :=
+@[to_dual instHImp]
+instance Pi.instSDiff [∀ i, SDiff (π i)] : SDiff (∀ i, π i) :=
   ⟨fun x y i ↦ x i \ y i⟩
 
-@[push ←]
+@[to_dual (attr := push ←) himp_def]
 theorem Pi.sdiff_def [∀ i, SDiff (π i)] (x y : ∀ i, π i) :
     x \ y = fun i ↦ x i \ y i :=
   rfl
 
-@[simp]
+@[to_dual (attr := simp) himp_apply]
 theorem Pi.sdiff_apply [∀ i, SDiff (π i)] (x y : ∀ i, π i) (i : ι) :
     (x \ y) i = x i \ y i :=
   rfl

Mathlib/Order/BooleanAlgebra/Basic.lean

@@ -352,7 +352,7 @@ lemma inf_sdiff_left_comm (a b c : α) : a ⊓ (b \ c) = b ⊓ (a \ c) := by
   simp_rw [← inf_sdiff_assoc, inf_comm]
 
 theorem inf_sdiff_distrib_left (a b c : α) : a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c) := by
-  rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
+  rw [sdiff_inf, (sdiff_eq_bot_iff (α := α)).2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
 
 theorem inf_sdiff_distrib_right (a b c : α) : a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c) := by
   simp_rw [inf_comm _ c, inf_sdiff_distrib_left]

Mathlib/Order/Disjoint.lean

@@ -307,6 +307,7 @@ section DistribLattice
 
 variable [DistribLattice α] [BoundedOrder α] {a b c : α}
 
+@[to_dual]
 theorem Disjoint.le_of_codisjoint (hab : Disjoint a b) (hbc : Codisjoint b c) : a ≤ c := by
   rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]
   exact inf_le_inf_right _ le_sup_left

Mathlib/Order/GaloisConnection/Basic.lean

@@ -119,7 +119,6 @@ end CompleteLattice
 -- Constructing Galois connections
 section Constructions
 
-@[to_dual self]
 protected theorem compl [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α}
     (gc : GaloisConnection l u) :
     GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl) := fun a b ↦ by