refactor: Make Frame extend HeytingAlgebra (#10560)

It is mathematically true that a frame is a Heyting algebra. However we want nice defeqs, so we can't just provide an instance defining `himp` as some supremum. Instead, we need `Frame` to directly extend `HeytingAlgebra`.




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: YaelDillies

Archive/Imo/Imo1998Q2.lean

@@ -116,7 +116,7 @@ theorem A_fibre_over_contestant_card (c : C) :
   apply Finset.card_image_of_injOn
   unfold Set.InjOn
   rintro ⟨a, p⟩ h ⟨a', p'⟩ h' rfl
-  aesop
+  aesop (add simp AgreedTriple.contestant)
 
 theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) :
     agreedContestants r p = ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).image

Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean

@@ -61,6 +61,9 @@ instance : Sup G.Finsubgraph :=
 instance : Inf G.Finsubgraph :=
   ⟨fun G₁ G₂ => ⟨G₁ ⊓ G₂, G₁.2.subset inter_subset_left⟩⟩
 
+instance instSDiff : SDiff G.Finsubgraph where
+  sdiff G₁ G₂ := ⟨G₁ \ G₂, G₁.2.subset (Subgraph.verts_mono sdiff_le)⟩
+
 @[simp, norm_cast] lemma coe_bot : (⊥ : G.Finsubgraph) = (⊥ : G.Subgraph) := rfl
 
 @[simp, norm_cast]
@@ -69,17 +72,28 @@ lemma coe_sup (G₁ G₂ : G.Finsubgraph) : ↑(G₁ ⊔ G₂) = (G₁ ⊔ G₂
 @[simp, norm_cast]
 lemma coe_inf (G₁ G₂ : G.Finsubgraph) : ↑(G₁ ⊓ G₂) = (G₁ ⊓ G₂ : G.Subgraph) := rfl
 
-instance : DistribLattice G.Finsubgraph :=
-  Subtype.coe_injective.distribLattice _ (fun _ _ => rfl) fun _ _ => rfl
+@[simp, norm_cast]
+lemma coe_sdiff (G₁ G₂ : G.Finsubgraph) : ↑(G₁ \ G₂) = (G₁ \ G₂ : G.Subgraph) := rfl
+
+instance instGeneralizedCoheytingAlgebra : GeneralizedCoheytingAlgebra G.Finsubgraph :=
+  Subtype.coe_injective.generalizedCoheytingAlgebra _ coe_sup coe_inf coe_bot coe_sdiff
 
 section Finite
 variable [Finite V]
 
 instance instTop : Top G.Finsubgraph where top := ⟨⊤, finite_univ⟩
+instance instHasCompl : HasCompl G.Finsubgraph where compl G' := ⟨G'ᶜ, Set.toFinite _⟩
+instance instHNot : HNot G.Finsubgraph where hnot G' := ⟨￢G', Set.toFinite _⟩
+instance instHImp : HImp G.Finsubgraph where himp G₁ G₂ := ⟨G₁ ⇨ G₂, Set.toFinite _⟩
 instance instSupSet : SupSet G.Finsubgraph where sSup s := ⟨⨆ G ∈ s, ↑G, Set.toFinite _⟩
 instance instInfSet : InfSet G.Finsubgraph where sInf s := ⟨⨅ G ∈ s, ↑G, Set.toFinite _⟩
 
-@[simp, norm_cast] lemma coe_top : ↑(⊤ : G.Finsubgraph) = (⊤ : G.Subgraph) := rfl
+@[simp, norm_cast] lemma coe_top : (⊤ : G.Finsubgraph) = (⊤ : G.Subgraph) := rfl
+@[simp, norm_cast] lemma coe_compl (G' : G.Finsubgraph) : ↑(G'ᶜ) = (G'ᶜ : G.Subgraph) := rfl
+@[simp, norm_cast] lemma coe_hnot (G' : G.Finsubgraph) : ↑(￢G') = (￢G' : G.Subgraph) := rfl
+
+@[simp, norm_cast]
+lemma coe_himp (G₁ G₂ : G.Finsubgraph) : ↑(G₁ ⇨ G₂) = (G₁ ⇨ G₂ : G.Subgraph) := rfl
 
 @[simp, norm_cast]
 lemma coe_sSup (s : Set G.Finsubgraph) : sSup s = (⨆ G ∈ s, G : G.Subgraph) := rfl
@@ -97,6 +111,7 @@ lemma coe_iInf {ι : Sort*} (f : ι → G.Finsubgraph) : ⨅ i, f i = (⨅ i, f
 
 instance instCompletelyDistribLattice : CompletelyDistribLattice G.Finsubgraph :=
   Subtype.coe_injective.completelyDistribLattice _ coe_sup coe_inf coe_sSup coe_sInf coe_top coe_bot
+    coe_compl coe_himp coe_hnot coe_sdiff
 
 end Finite
 end Finsubgraph

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -397,8 +397,8 @@ instance : BoundedOrder (Subgraph G) where
   le_top x := ⟨Set.subset_univ _, fun _ _ => x.adj_sub⟩
   bot_le _ := ⟨Set.empty_subset _, fun _ _ => False.elim⟩
 
--- Note that subgraphs do not form a Boolean algebra, because of `verts`.
-instance : CompletelyDistribLattice G.Subgraph :=
+/-- Note that subgraphs do not form a Boolean algebra, because of `verts`. -/
+def completelyDistribLatticeMinimalAxioms : CompletelyDistribLattice.MinimalAxioms G.Subgraph :=
   { Subgraph.distribLattice with
     le := (· ≤ ·)
     sup := (· ⊔ ·)
@@ -422,6 +422,9 @@ instance : CompletelyDistribLattice G.Subgraph :=
     iInf_iSup_eq := fun f => Subgraph.ext _ _ (by simpa using iInf_iSup_eq)
       (by ext; simp [Classical.skolem]) }
 
+instance : CompletelyDistribLattice G.Subgraph :=
+  .ofMinimalAxioms completelyDistribLatticeMinimalAxioms
+
 @[gcongr] lemma verts_mono {H H' : G.Subgraph} (h : H ≤ H') : H.verts ⊆ H'.verts := h.1
 lemma verts_monotone : Monotone (verts : G.Subgraph → Set V) := fun _ _ h ↦ h.1
 

Mathlib/Data/Fintype/Order.lean

@@ -91,11 +91,10 @@ noncomputable abbrev toCompleteLattice [Lattice α] [BoundedOrder α] : Complete
   sInf_le := fun _ _ ha => Finset.inf_le (Set.mem_toFinset.mpr ha)
   le_sInf := fun s _ ha => Finset.le_inf fun b hb => ha _ <| Set.mem_toFinset.mp hb
 
--- Porting note: `convert` doesn't work as well as it used to.
 -- See note [reducible non-instances]
 /-- A finite bounded distributive lattice is completely distributive. -/
-noncomputable abbrev toCompleteDistribLattice [DistribLattice α] [BoundedOrder α] :
-    CompleteDistribLattice α where
+noncomputable abbrev toCompleteDistribLatticeMinimalAxioms [DistribLattice α] [BoundedOrder α] :
+    CompleteDistribLattice.MinimalAxioms α where
   __ := toCompleteLattice α
   iInf_sup_le_sup_sInf := fun a s => by
     convert (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
@@ -108,6 +107,11 @@ noncomputable abbrev toCompleteDistribLattice [DistribLattice α] [BoundedOrder
     simp_rw [Set.mem_toFinset]
     rfl
 
+-- See note [reducible non-instances]
+/-- A finite bounded distributive lattice is completely distributive. -/
+noncomputable abbrev toCompleteDistribLattice [DistribLattice α] [BoundedOrder α] :
+    CompleteDistribLattice α := .ofMinimalAxioms (toCompleteDistribLatticeMinimalAxioms _)
+
 -- See note [reducible non-instances]
 /-- A finite bounded linear order is complete. -/
 noncomputable abbrev toCompleteLinearOrder

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -1287,6 +1287,7 @@ theorem coe_top : ↑(⊤ : Subtype (MeasurableSet : Set α → Prop)) = (⊤ :
 noncomputable instance Subtype.instBooleanAlgebra :
     BooleanAlgebra (Subtype (MeasurableSet : Set α → Prop)) :=
   Subtype.coe_injective.booleanAlgebra _ coe_union coe_inter coe_top coe_bot coe_compl coe_sdiff
+    coe_himp
 
 @[measurability]
 theorem measurableSet_blimsup {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ n, p n → MeasurableSet (s n)) :

Mathlib/ModelTheory/Definability.lean

@@ -377,9 +377,9 @@ theorem coe_sdiff (s t : L.DefinableSet A α) :
 @[simp, norm_cast]
 lemma coe_himp (s t : L.DefinableSet A α) : ↑(s ⇨ t) = (s ⇨ t : Set (α → M)) := rfl
 
-instance instBooleanAlgebra : BooleanAlgebra (L.DefinableSet A α) :=
+noncomputable instance instBooleanAlgebra : BooleanAlgebra (L.DefinableSet A α) :=
   Function.Injective.booleanAlgebra (α := L.DefinableSet A α) _ Subtype.coe_injective
-    coe_sup coe_inf coe_top coe_bot coe_compl coe_sdiff
+    coe_sup coe_inf coe_top coe_bot coe_compl coe_sdiff coe_himp
 
 end DefinableSet
 

Mathlib/Order/BooleanAlgebra.lean

@@ -751,12 +751,14 @@ protected abbrev Function.Injective.generalizedBooleanAlgebra [Sup α] [Inf α]
 -- See note [reducible non-instances]
 /-- Pullback a `BooleanAlgebra` along an injection. -/
 protected abbrev Function.Injective.booleanAlgebra [Sup α] [Inf α] [Top α] [Bot α] [HasCompl α]
-    [SDiff α] [BooleanAlgebra β] (f : α → β) (hf : Injective f)
+    [SDiff α] [HImp α] [BooleanAlgebra β] (f : α → β) (hf : Injective f)
     (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
     (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
-    (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : BooleanAlgebra α where
+    (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) :
+    BooleanAlgebra α where
   __ := hf.generalizedBooleanAlgebra f map_sup map_inf map_bot map_sdiff
   compl := compl
+  himp := himp
   top := ⊤
   le_top a := (@le_top β _ _ _).trans map_top.ge
   bot_le a := map_bot.le.trans bot_le
@@ -765,6 +767,7 @@ protected abbrev Function.Injective.booleanAlgebra [Sup α] [Inf α] [Top α] [B
   sdiff_eq a b := by
     refine hf ((map_sdiff _ _).trans (sdiff_eq.trans ?_))
     rw [map_inf, map_compl]
+  himp_eq a b := hf $ (map_himp _ _).trans $ himp_eq.trans $ by rw [map_sup, map_compl]
 
 end lift