text:
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.analysis.filter
! leanprover-community/mathlib commit 34ee86e6a59d911a8e4f89b68793ee7577ae79c7
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Order.Filter.Cofinite

/-!
# Computational realization of filters (experimental)

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

This file provides infrastructure to compute with filters.

## Main declarations

* `cfilter`: Realization of a filter base. Note that this is in the generality of filters on
  lattices, while `filter` is filters of sets (so corresponding to `cfilter (set α) σ`).
* `filter.realizer`: Realization of a `filter`. `cfilter` that generates the given filter.
-/

open Set Filter

#print CFilter /-
/-- A `cfilter α σ` is a realization of a filter (base) on `α`,
  represented by a type `σ` together with operations for the top element and
  the binary inf operation. -/
structure CFilter (α σ : Type _) [PartialOrder α] where
  f : σ → α
  pt : σ
  inf : σ → σ → σ
  inf_le_left : ∀ a b : σ, f (inf a b) ≤ f a
  inf_le_right : ∀ a b : σ, f (inf a b) ≤ f b
#align cfilter CFilter
-/

variable {α : Type _} {β : Type _} {σ : Type _} {τ : Type _}

instance [Inhabited α] [SemilatticeInf α] : Inhabited (CFilter α α) :=
  ⟨{  f := id
      pt := default
      inf := (· ⊓ ·)
      inf_le_left := fun _ _ => inf_le_left
      inf_le_right := fun _ _ => inf_le_right }⟩

namespace CFilter

section

variable [PartialOrder α] (F : CFilter α σ)

instance : CoeFun (CFilter α σ) fun _ => σ → α :=
  ⟨CFilter.f⟩

/- warning: cfilter.coe_mk -> CFilter.coe_mk is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {σ : Type.{u2}} [_inst_1 : PartialOrder.{u1} α] (f : σ -> α) (pt : σ) (inf : σ -> σ -> σ) (h₁ : forall (a : σ) (b : σ), LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α _inst_1)) (f (inf a b)) (f a)) (h₂ : forall (a : σ) (b : σ), LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α _inst_1)) (f (inf a b)) (f b)) (a : σ), Eq.{succ u1} α (coeFn.{max (succ u1) (succ u2), max (succ u2) (succ u1)} (CFilter.{u1, u2} α σ _inst_1) (fun (_x : CFilter.{u1, u2} α σ _inst_1) => σ -> α) (CFilter.hasCoeToFun.{u1, u2} α σ _inst_1) (CFilter.mk.{u1, u2} α σ _inst_1 f pt inf h₁ h₂) a) (f a)
but is expected to have type
  forall {α : Type.{u2}} {σ : Type.{u1}} [_inst_1 : PartialOrder.{u2} α] (f : σ -> α) (pt : σ) (inf : σ -> σ -> σ) (h₁ : forall (a : σ) (b : σ), LE.le.{u2} α (Preorder.toLE.{u2} α (PartialOrder.toPreorder.{u2} α _inst_1)) (f (inf a b)) (f a)) (h₂ : forall (a : σ) (b : σ), LE.le.{u2} α (Preorder.toLE.{u2} α (PartialOrder.toPreorder.{u2} α _inst_1)) (f (inf a b)) (f b)) (a : σ), Eq.{succ u2} α (CFilter.f.{u2, u1} α σ _inst_1 (CFilter.mk.{u2, u1} α σ _inst_1 f pt inf h₁ h₂) a) (f a)
Case conversion may be inaccurate. Consider using '#align cfilter.coe_mk CFilter.coe_mkₓ'. -/
@[simp]
theorem coe_mk (f pt inf h₁ h₂ a) : (@CFilter.mk α σ _ f pt inf h₁ h₂) a = f a :=
  rfl
#align cfilter.coe_mk CFilter.coe_mk

#print CFilter.ofEquiv /-
/-- Map a cfilter to an equivalent representation type. -/
def ofEquiv (E : σ ≃ τ) : CFilter α σ → CFilter α τ
  | ⟨f, p, g, h₁, h₂⟩ =>
    { f := fun a => f (E.symm a)
      pt := E p
      inf := fun a b => E (g (E.symm a) (E.symm b))
      inf_le_left := fun a b => by simpa using h₁ (E.symm a) (E.symm b)
      inf_le_right := fun a b => by simpa using h₂ (E.symm a) (E.symm b) }
#align cfilter.of_equiv CFilter.ofEquiv
-/

/- warning: cfilter.of_equiv_val -> CFilter.ofEquiv_val is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {σ : Type.{u2}} {τ : Type.{u3}} [_inst_1 : PartialOrder.{u1} α] (E : Equiv.{succ u2, succ u3} σ τ) (F : CFilter.{u1, u2} α σ _inst_1) (a : τ), Eq.{succ u1} α (coeFn.{max (succ u1) (succ u3), max (succ u3) (succ u1)} (CFilter.{u1, u3} α τ _inst_1) (fun (_x : CFilter.{u1, u3} α τ _inst_1) => τ -> α) (CFilter.hasCoeToFun.{u1, u3} α τ _inst_1) (CFilter.ofEquiv.{u1, u2, u3} α σ τ _inst_1 E F) a) (coeFn.{max (succ u1) (succ u2), max (succ u2) (succ u1)} (CFilter.{u1, u2} α σ _inst_1) (fun (_x : CFilter.{u1, u2} α σ _inst_1) => σ -> α) (CFilter.hasCoeToFun.{u1, u2} α σ _inst_1) F (coeFn.{max 1 (max (succ u3) (succ u2)) (succ u2) (succ u3), max (succ u3) (succ u2)} (Equiv.{succ u3, succ u2} τ σ) (fun (_x : Equiv.{succ u3, succ u2} τ σ) => τ -> σ) (Equiv.hasCoeToFun.{succ u3, succ u2} τ σ) (Equiv.symm.{succ u2, succ u3} σ τ E) a))
but is expected to have type
  forall {α : Type.{u1}} {σ : Type.{u3}} {τ : Type.{u2}} [_inst_1 : PartialOrder.{u1} α] (E : Equiv.{succ u3, succ u2} σ τ) (F : CFilter.{u1, u3} α σ _inst_1) (a : τ), Eq.{succ u1} α (CFilter.f.{u1, u2} α τ _inst_1 (CFilter.ofEquiv.{u1, u3, u2} α σ τ _inst_1 E F) a) (CFilter.f.{u1, u3} α σ _inst_1 F (FunLike.coe.{max (succ u3) (succ u2), succ u2, succ u3} (Equiv.{succ u2, succ u3} τ σ) τ (fun (_x : τ) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : τ) => σ) _x) (Equiv.instFunLikeEquiv.{succ u2, succ u3} τ σ) (Equiv.symm.{succ u3, succ u2} σ τ E) a))
Case conversion may be inaccurate. Consider using '#align cfilter.of_equiv_val CFilter.ofEquiv_valₓ'. -/
@[simp]
theorem ofEquiv_val (E : σ ≃ τ) (F : CFilter α σ) (a : τ) : F.of_equiv E a = F (E.symm a) := by
  cases F <;> rfl
#align cfilter.of_equiv_val CFilter.ofEquiv_val

end

/- warning: cfilter.to_filter -> CFilter.toFilter is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {σ : Type.{u2}}, (CFilter.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) -> (Filter.{u1} α)
but is expected to have type
  forall {α : Type.{u1}} {σ : Type.{u2}}, (CFilter.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.instCompleteBooleanAlgebraSet.{u1} α))))))) -> (Filter.{u1} α)
Case conversion may be inaccurate. Consider using '#align cfilter.to_filter CFilter.toFilterₓ'. -/
/-- The filter represented by a `cfilter` is the collection of supersets of
  elements of the filter base. -/
def toFilter (F : CFilter (Set α) σ) : Filter α
    where
  sets := { a | ∃ b, F b ⊆ a }
  univ_sets := ⟨F.pt, subset_univ _⟩
  sets_of_superset := fun x y ⟨b, h⟩ s => ⟨b, Subset.trans h s⟩
  inter_sets := fun x y ⟨a, h₁⟩ ⟨b, h₂⟩ =>
    ⟨F.inf a b,
      subset_inter (Subset.trans (F.inf_le_left _ _) h₁) (Subset.trans (F.inf_le_right _ _) h₂)⟩
#align cfilter.to_filter CFilter.toFilter

/- warning: cfilter.mem_to_filter_sets -> CFilter.mem_toFilter_sets is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {σ : Type.{u2}} (F : CFilter.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) {a : Set.{u1} α}, Iff (Membership.Mem.{u1, u1} (Set.{u1} α) (Filter.{u1} α) (Filter.hasMem.{u1} α) a (CFilter.toFilter.{u1, u2} α σ F)) (Exists.{succ u2} σ (fun (b : σ) => HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) (coeFn.{max (succ u1) (succ u2), max (succ u2) (succ u1)} (CFilter.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => σ -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) F b) a))
but is expected to have type
  forall {α : Type.{u2}} {σ : Type.{u1}} (F : CFilter.{u2, u1} (Set.{u2} α) σ (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} α) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} α) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} α) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} α) (Set.instCompleteBooleanAlgebraSet.{u2} α))))))) {a : Set.{u2} α}, Iff (Membership.mem.{u2, u2} (Set.{u2} α) (Filter.{u2} α) (instMembershipSetFilter.{u2} α) a (CFilter.toFilter.{u2, u1} α σ F)) (Exists.{succ u1} σ (fun (b : σ) => HasSubset.Subset.{u2} (Set.{u2} α) (Set.instHasSubsetSet.{u2} α) (CFilter.f.{u2, u1} (Set.{u2} α) σ (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} α) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} α) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} α) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} α) (Set.instCompleteBooleanAlgebraSet.{u2} α)))))) F b) a))
Case conversion may be inaccurate. Consider using '#align cfilter.mem_to_filter_sets CFilter.mem_toFilter_setsₓ'. -/
@[simp]
theorem mem_toFilter_sets (F : CFilter (Set α) σ) {a : Set α} : a ∈ F.toFilter ↔ ∃ b, F b ⊆ a :=
  Iff.rfl
#align cfilter.mem_to_filter_sets CFilter.mem_toFilter_sets

end CFilter

#print Filter.Realizer /-
/-- A realizer for filter `f` is a cfilter which generates `f`. -/
structure Filter.Realizer (f : Filter α) where
  σ : Type _
  f : CFilter (Set α) σ
  Eq : F.toFilter = f
#align filter.realizer Filter.Realizer
-/

/- warning: cfilter.to_realizer -> CFilter.toRealizer is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {σ : Type.{u2}} (F : CFilter.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))), Filter.Realizer.{u1, u2} α (CFilter.toFilter.{u1, u2} α σ F)
but is expected to have type
  forall {α : Type.{u1}} {σ : Type.{u2}} (F : CFilter.{u1, u2} (Set.{u1} α) σ (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.instCompleteBooleanAlgebraSet.{u1} α))))))), Filter.Realizer.{u1, u2} α (CFilter.toFilter.{u1, u2} α σ F)
Case conversion may be inaccurate. Consider using '#align cfilter.to_realizer CFilter.toRealizerₓ'. -/
/-- A `cfilter` realizes the filter it generates. -/
protected def CFilter.toRealizer (F : CFilter (Set α) σ) : F.toFilter.Realizer :=
  ⟨σ, F, rfl⟩
#align cfilter.to_realizer CFilter.toRealizer

namespace Filter.Realizer

/- warning: filter.realizer.mem_sets -> Filter.Realizer.mem_sets is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {f : Filter.{u1} α} (F : Filter.Realizer.{u1, u2} α f) {a : Set.{u1} α}, Iff (Membership.Mem.{u1, u1} (Set.{u1} α) (Filter.{u1} α) (Filter.hasMem.{u1} α) a f) (Exists.{succ u2} (Filter.Realizer.σ.{u1, u2} α f F) (fun (b : Filter.Realizer.σ.{u1, u2} α f F) => HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) (coeFn.{max (succ u1) (succ u2), max (succ u2) (succ u1)} (CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u2} α f F) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u2} α f F) b) a))
but is expected to have type
  forall {α : Type.{u2}} {f : Filter.{u2} α} (F : Filter.Realizer.{u2, u1} α f) {a : Set.{u2} α}, Iff (Membership.mem.{u2, u2} (Set.{u2} α) (Filter.{u2} α) (instMembershipSetFilter.{u2} α) a f) (Exists.{succ u1} (Filter.Realizer.σ.{u2, u1} α f F) (fun (b : Filter.Realizer.σ.{u2, u1} α f F) => HasSubset.Subset.{u2} (Set.{u2} α) (Set.instHasSubsetSet.{u2} α) (CFilter.f.{u2, u1} (Set.{u2} α) (Filter.Realizer.σ.{u2, u1} α f F) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} α) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} α) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} α) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} α) (Set.instCompleteBooleanAlgebraSet.{u2} α)))))) (Filter.Realizer.F.{u2, u1} α f F) b) a))
Case conversion may be inaccurate. Consider using '#align filter.realizer.mem_sets Filter.Realizer.mem_setsₓ'. -/
theorem mem_sets {f : Filter α} (F : f.Realizer) {a : Set α} : a ∈ f ↔ ∃ b, F.f b ⊆ a := by
  cases F <;> subst f <;> simp
#align filter.realizer.mem_sets Filter.Realizer.mem_sets

#print Filter.Realizer.ofEq /-
/-- Transfer a realizer along an equality of filter. This has better definitional equalities than
the `eq.rec` proof. -/
def ofEq {f g : Filter α} (e : f = g) (F : f.Realizer) : g.Realizer :=
  ⟨F.σ, F.f, F.Eq.trans e⟩
#align filter.realizer.of_eq Filter.Realizer.ofEq
-/

#print Filter.Realizer.ofFilter /-
/-- A filter realizes itself. -/
def ofFilter (f : Filter α) : f.Realizer :=
  ⟨f.sets,
    { f := Subtype.val
      pt := ⟨univ, univ_mem⟩
      inf := fun ⟨x, h₁⟩ ⟨y, h₂⟩ => ⟨_, inter_mem h₁ h₂⟩
      inf_le_left := fun ⟨x, h₁⟩ ⟨y, h₂⟩ => inter_subset_left x y
      inf_le_right := fun ⟨x, h₁⟩ ⟨y, h₂⟩ => inter_subset_right x y },
    filter_eq <| Set.ext fun x => SetCoe.exists.trans exists_mem_subset_iff⟩
#align filter.realizer.of_filter Filter.Realizer.ofFilter
-/

#print Filter.Realizer.ofEquiv /-
/-- Transfer a filter realizer to another realizer on a different base type. -/
def ofEquiv {f : Filter α} (F : f.Realizer) (E : F.σ ≃ τ) : f.Realizer :=
  ⟨τ, F.f.of_equiv E, by
    refine' Eq.trans _ F.eq <;>
      exact
        filter_eq
          (Set.ext fun x =>
            ⟨fun ⟨s, h⟩ => ⟨E.symm s, by simpa using h⟩, fun ⟨t, h⟩ => ⟨E t, by simp [h]⟩⟩)⟩
#align filter.realizer.of_equiv Filter.Realizer.ofEquiv
-/

/- warning: filter.realizer.of_equiv_σ -> Filter.Realizer.ofEquiv_σ is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {τ : Type.{u2}} {f : Filter.{u1} α} (F : Filter.Realizer.{u1, u3} α f) (E : Equiv.{succ u3, succ u2} (Filter.Realizer.σ.{u1, u3} α f F) τ), Eq.{succ (succ u2)} Type.{u2} (Filter.Realizer.σ.{u1, u2} α f (Filter.Realizer.ofEquiv.{u1, u2, u3} α τ f F E)) τ
but is expected to have type
  forall {α : Type.{u3}} {τ : Type.{u1}} {f : Filter.{u3} α} (F : Filter.Realizer.{u3, u2} α f) (E : Equiv.{succ u2, succ u1} (Filter.Realizer.σ.{u3, u2} α f F) τ), Eq.{succ (succ u1)} Type.{u1} (Filter.Realizer.σ.{u3, u1} α f (Filter.Realizer.ofEquiv.{u3, u1, u2} α τ f F E)) τ
Case conversion may be inaccurate. Consider using '#align filter.realizer.of_equiv_σ Filter.Realizer.ofEquiv_σₓ'. -/
@[simp]
theorem ofEquiv_σ {f : Filter α} (F : f.Realizer) (E : F.σ ≃ τ) : (F.of_equiv E).σ = τ :=
  rfl
#align filter.realizer.of_equiv_σ Filter.Realizer.ofEquiv_σ

/- warning: filter.realizer.of_equiv_F -> Filter.Realizer.ofEquiv_F is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {τ : Type.{u2}} {f : Filter.{u1} α} (F : Filter.Realizer.{u1, u3} α f) (E : Equiv.{succ u3, succ u2} (Filter.Realizer.σ.{u1, u3} α f F) τ) (s : τ), Eq.{succ u1} (Set.{u1} α) (coeFn.{max (succ u1) (succ u2), max (succ u2) (succ u1)} (CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f (Filter.Realizer.ofEquiv.{u1, u2, u3} α τ f F E)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f (Filter.Realizer.ofEquiv.{u1, u2, u3} α τ f F E)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u2} α f (Filter.Realizer.ofEquiv.{u1, u2, u3} α τ f F E)) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f (Filter.Realizer.ofEquiv.{u1, u2, u3} α τ f F E)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u2} α f (Filter.Realizer.ofEquiv.{u1, u2, u3} α τ f F E)) s) (coeFn.{max (succ u1) (succ u3), max (succ u3) (succ u1)} (CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u3} α f F) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u3} α f F) (coeFn.{max 1 (max (succ u2) (succ u3)) (succ u3) (succ u2), max (succ u2) (succ u3)} (Equiv.{succ u2, succ u3} τ (Filter.Realizer.σ.{u1, u3} α f F)) (fun (_x : Equiv.{succ u2, succ u3} τ (Filter.Realizer.σ.{u1, u3} α f F)) => τ -> (Filter.Realizer.σ.{u1, u3} α f F)) (Equiv.hasCoeToFun.{succ u2, succ u3} τ (Filter.Realizer.σ.{u1, u3} α f F)) (Equiv.symm.{succ u3, succ u2} (Filter.Realizer.σ.{u1, u3} α f F) τ E) s))
but is expected to have type
  forall {α : Type.{u3}} {τ : Type.{u1}} {f : Filter.{u3} α} (F : Filter.Realizer.{u3, u2} α f) (E : Equiv.{succ u2, succ u1} (Filter.Realizer.σ.{u3, u2} α f F) τ) (s : τ), Eq.{succ u3} (Set.{u3} α) (CFilter.f.{u3, u1} (Set.{u3} α) (Filter.Realizer.σ.{u3, u1} α f (Filter.Realizer.ofEquiv.{u3, u1, u2} α τ f F E)) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} α) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} α) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} α) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} α) (Set.instCompleteBooleanAlgebraSet.{u3} α)))))) (Filter.Realizer.F.{u3, u1} α f (Filter.Realizer.ofEquiv.{u3, u1, u2} α τ f F E)) s) (CFilter.f.{u3, u2} (Set.{u3} α) (Filter.Realizer.σ.{u3, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} α) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} α) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} α) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} α) (Set.instCompleteBooleanAlgebraSet.{u3} α)))))) (Filter.Realizer.F.{u3, u2} α f F) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (Equiv.{succ u1, succ u2} τ (Filter.Realizer.σ.{u3, u2} α f F)) τ (fun (_x : τ) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : τ) => Filter.Realizer.σ.{u3, u2} α f F) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u2} τ (Filter.Realizer.σ.{u3, u2} α f F)) (Equiv.symm.{succ u2, succ u1} (Filter.Realizer.σ.{u3, u2} α f F) τ E) s))
Case conversion may be inaccurate. Consider using '#align filter.realizer.of_equiv_F Filter.Realizer.ofEquiv_Fₓ'. -/
@[simp]
theorem ofEquiv_F {f : Filter α} (F : f.Realizer) (E : F.σ ≃ τ) (s : τ) :
    (F.of_equiv E).f s = F.f (E.symm s) := by delta of_equiv <;> simp
#align filter.realizer.of_equiv_F Filter.Realizer.ofEquiv_F

#print Filter.Realizer.principal /-
/-- `unit` is a realizer for the principal filter -/
protected def principal (s : Set α) : (principal s).Realizer :=
  ⟨Unit,
    { f := fun _ => s
      pt := ()
      inf := fun _ _ => ()
      inf_le_left := fun _ _ => le_rfl
      inf_le_right := fun _ _ => le_rfl },
    filter_eq <| Set.ext fun x => ⟨fun ⟨_, s⟩ => s, fun h => ⟨(), h⟩⟩⟩
#align filter.realizer.principal Filter.Realizer.principal
-/

#print Filter.Realizer.principal_σ /-
@[simp]
theorem principal_σ (s : Set α) : (Realizer.principal s).σ = Unit :=
  rfl
#align filter.realizer.principal_σ Filter.Realizer.principal_σ
-/

/- warning: filter.realizer.principal_F -> Filter.Realizer.principal_F is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} (s : Set.{u1} α) (u : Unit), Eq.{succ u1} (Set.{u1} α) (coeFn.{succ u1, succ u1} (CFilter.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Filter.principal.{u1} α s) (Filter.Realizer.principal.{u1} α s)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Filter.principal.{u1} α s) (Filter.Realizer.principal.{u1} α s)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, 0} α (Filter.principal.{u1} α s) (Filter.Realizer.principal.{u1} α s)) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Filter.principal.{u1} α s) (Filter.Realizer.principal.{u1} α s)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, 0} α (Filter.principal.{u1} α s) (Filter.Realizer.principal.{u1} α s)) u) s
but is expected to have type
  forall {α : Type.{u1}} (s : Set.{u1} α) (u : Unit), Eq.{succ u1} (Set.{u1} α) (CFilter.f.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Filter.principal.{u1} α s) (Filter.Realizer.principal.{u1} α s)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.instCompleteBooleanAlgebraSet.{u1} α)))))) (Filter.Realizer.F.{u1, 0} α (Filter.principal.{u1} α s) (Filter.Realizer.principal.{u1} α s)) u) s
Case conversion may be inaccurate. Consider using '#align filter.realizer.principal_F Filter.Realizer.principal_Fₓ'. -/
@[simp]
theorem principal_F (s : Set α) (u : Unit) : (Realizer.principal s).f u = s :=
  rfl
#align filter.realizer.principal_F Filter.Realizer.principal_F

instance (s : Set α) : Inhabited (principal s).Realizer :=
  ⟨Realizer.principal s⟩

/- warning: filter.realizer.top -> Filter.Realizer.top is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}}, Filter.Realizer.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.hasTop.{u1} α))
but is expected to have type
  forall {α : Type.{u1}}, Filter.Realizer.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.instTopFilter.{u1} α))
Case conversion may be inaccurate. Consider using '#align filter.realizer.top Filter.Realizer.topₓ'. -/
/-- `unit` is a realizer for the top filter -/
protected def top : (⊤ : Filter α).Realizer :=
  (Realizer.principal _).of_eq principal_univ
#align filter.realizer.top Filter.Realizer.top

#print Filter.Realizer.top_σ /-
@[simp]
theorem top_σ : (@Realizer.top α).σ = Unit :=
  rfl
#align filter.realizer.top_σ Filter.Realizer.top_σ
-/

/- warning: filter.realizer.top_F -> Filter.Realizer.top_F is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} (u : Unit), Eq.{succ u1} (Set.{u1} α) (coeFn.{succ u1, succ u1} (CFilter.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.hasTop.{u1} α)) (Filter.Realizer.top.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.hasTop.{u1} α)) (Filter.Realizer.top.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.hasTop.{u1} α)) (Filter.Realizer.top.{u1} α)) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.hasTop.{u1} α)) (Filter.Realizer.top.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.hasTop.{u1} α)) (Filter.Realizer.top.{u1} α)) u) (Set.univ.{u1} α)
but is expected to have type
  forall {α : Type.{u1}} (u : Unit), Eq.{succ u1} (Set.{u1} α) (CFilter.f.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.instTopFilter.{u1} α)) (Filter.Realizer.top.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.instCompleteBooleanAlgebraSet.{u1} α)))))) (Filter.Realizer.F.{u1, 0} α (Top.top.{u1} (Filter.{u1} α) (Filter.instTopFilter.{u1} α)) (Filter.Realizer.top.{u1} α)) u) (Set.univ.{u1} α)
Case conversion may be inaccurate. Consider using '#align filter.realizer.top_F Filter.Realizer.top_Fₓ'. -/
@[simp]
theorem top_F (u : Unit) : (@Realizer.top α).f u = univ :=
  rfl
#align filter.realizer.top_F Filter.Realizer.top_F

/- warning: filter.realizer.bot -> Filter.Realizer.bot is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}}, Filter.Realizer.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toHasBot.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α)))
but is expected to have type
  forall {α : Type.{u1}}, Filter.Realizer.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toBot.{u1} (Filter.{u1} α) (Filter.instCompleteLatticeFilter.{u1} α)))
Case conversion may be inaccurate. Consider using '#align filter.realizer.bot Filter.Realizer.botₓ'. -/
/-- `unit` is a realizer for the bottom filter -/
protected def bot : (⊥ : Filter α).Realizer :=
  (Realizer.principal _).of_eq principal_empty
#align filter.realizer.bot Filter.Realizer.bot

#print Filter.Realizer.bot_σ /-
@[simp]
theorem bot_σ : (@Realizer.bot α).σ = Unit :=
  rfl
#align filter.realizer.bot_σ Filter.Realizer.bot_σ
-/

/- warning: filter.realizer.bot_F -> Filter.Realizer.bot_F is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} (u : Unit), Eq.{succ u1} (Set.{u1} α) (coeFn.{succ u1, succ u1} (CFilter.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toHasBot.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α))) (Filter.Realizer.bot.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toHasBot.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α))) (Filter.Realizer.bot.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toHasBot.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α))) (Filter.Realizer.bot.{u1} α)) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toHasBot.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α))) (Filter.Realizer.bot.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toHasBot.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α))) (Filter.Realizer.bot.{u1} α)) u) (EmptyCollection.emptyCollection.{u1} (Set.{u1} α) (Set.hasEmptyc.{u1} α))
but is expected to have type
  forall {α : Type.{u1}} (u : Unit), Eq.{succ u1} (Set.{u1} α) (CFilter.f.{u1, 0} (Set.{u1} α) (Filter.Realizer.σ.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toBot.{u1} (Filter.{u1} α) (Filter.instCompleteLatticeFilter.{u1} α))) (Filter.Realizer.bot.{u1} α)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.instCompleteBooleanAlgebraSet.{u1} α)))))) (Filter.Realizer.F.{u1, 0} α (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toBot.{u1} (Filter.{u1} α) (Filter.instCompleteLatticeFilter.{u1} α))) (Filter.Realizer.bot.{u1} α)) u) (EmptyCollection.emptyCollection.{u1} (Set.{u1} α) (Set.instEmptyCollectionSet.{u1} α))
Case conversion may be inaccurate. Consider using '#align filter.realizer.bot_F Filter.Realizer.bot_Fₓ'. -/
@[simp]
theorem bot_F (u : Unit) : (@Realizer.bot α).f u = ∅ :=
  rfl
#align filter.realizer.bot_F Filter.Realizer.bot_F

#print Filter.Realizer.map /-
/-- Construct a realizer for `map m f` given a realizer for `f` -/
protected def map (m : α → β) {f : Filter α} (F : f.Realizer) : (map m f).Realizer :=
  ⟨F.σ,
    { f := fun s => image m (F.f s)
      pt := F.f.pt
      inf := F.f.inf
      inf_le_left := fun a b => image_subset _ (F.f.inf_le_left _ _)
      inf_le_right := fun a b => image_subset _ (F.f.inf_le_right _ _) },
    filter_eq <| Set.ext fun x => by simp [CFilter.toFilter] <;> rw [F.mem_sets] <;> rfl⟩
#align filter.realizer.map Filter.Realizer.map
-/

/- warning: filter.realizer.map_σ -> Filter.Realizer.map_σ is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {β : Type.{u2}} (m : α -> β) {f : Filter.{u1} α} (F : Filter.Realizer.{u1, u3} α f), Eq.{succ (succ u3)} Type.{u3} (Filter.Realizer.σ.{u2, u3} β (Filter.map.{u1, u2} α β m f) (Filter.Realizer.map.{u1, u2, u3} α β m f F)) (Filter.Realizer.σ.{u1, u3} α f F)
but is expected to have type
  forall {α : Type.{u3}} {β : Type.{u1}} (m : α -> β) {f : Filter.{u3} α} (F : Filter.Realizer.{u3, u2} α f), Eq.{succ (succ u2)} Type.{u2} (Filter.Realizer.σ.{u1, u2} β (Filter.map.{u3, u1} α β m f) (Filter.Realizer.map.{u3, u1, u2} α β m f F)) (Filter.Realizer.σ.{u3, u2} α f F)
Case conversion may be inaccurate. Consider using '#align filter.realizer.map_σ Filter.Realizer.map_σₓ'. -/
@[simp]
theorem map_σ (m : α → β) {f : Filter α} (F : f.Realizer) : (F.map m).σ = F.σ :=
  rfl
#align filter.realizer.map_σ Filter.Realizer.map_σ

/- warning: filter.realizer.map_F -> Filter.Realizer.map_F is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {β : Type.{u2}} (m : α -> β) {f : Filter.{u1} α} (F : Filter.Realizer.{u1, u3} α f) (s : Filter.Realizer.σ.{u2, u3} β (Filter.map.{u1, u2} α β m f) (Filter.Realizer.map.{u1, u2, u3} α β m f F)), Eq.{succ u2} (Set.{u2} β) (coeFn.{max (succ u2) (succ u3), max (succ u3) (succ u2)} (CFilter.{u2, u3} (Set.{u2} β) (Filter.Realizer.σ.{u2, u3} β (Filter.map.{u1, u2} α β m f) (Filter.Realizer.map.{u1, u2, u3} α β m f F)) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} β) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} β) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} β) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} β) (Set.completeBooleanAlgebra.{u2} β))))))) (fun (_x : CFilter.{u2, u3} (Set.{u2} β) (Filter.Realizer.σ.{u2, u3} β (Filter.map.{u1, u2} α β m f) (Filter.Realizer.map.{u1, u2, u3} α β m f F)) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} β) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} β) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} β) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} β) (Set.completeBooleanAlgebra.{u2} β))))))) => (Filter.Realizer.σ.{u2, u3} β (Filter.map.{u1, u2} α β m f) (Filter.Realizer.map.{u1, u2, u3} α β m f F)) -> (Set.{u2} β)) (CFilter.hasCoeToFun.{u2, u3} (Set.{u2} β) (Filter.Realizer.σ.{u2, u3} β (Filter.map.{u1, u2} α β m f) (Filter.Realizer.map.{u1, u2, u3} α β m f F)) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} β) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} β) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} β) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} β) (Set.completeBooleanAlgebra.{u2} β))))))) (Filter.Realizer.f.{u2, u3} β (Filter.map.{u1, u2} α β m f) (Filter.Realizer.map.{u1, u2, u3} α β m f F)) s) (Set.image.{u1, u2} α β m (coeFn.{max (succ u1) (succ u3), max (succ u3) (succ u1)} (CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u3} α f F) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u3} α f F) s))
but is expected to have type
  forall {α : Type.{u3}} {β : Type.{u1}} (m : α -> β) {f : Filter.{u3} α} (F : Filter.Realizer.{u3, u2} α f) (s : Filter.Realizer.σ.{u1, u2} β (Filter.map.{u3, u1} α β m f) (Filter.Realizer.map.{u3, u1, u2} α β m f F)), Eq.{succ u1} (Set.{u1} β) (CFilter.f.{u1, u2} (Set.{u1} β) (Filter.Realizer.σ.{u1, u2} β (Filter.map.{u3, u1} α β m f) (Filter.Realizer.map.{u3, u1, u2} α β m f F)) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} β) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} β) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} β) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} β) (Set.instCompleteBooleanAlgebraSet.{u1} β)))))) (Filter.Realizer.F.{u1, u2} β (Filter.map.{u3, u1} α β m f) (Filter.Realizer.map.{u3, u1, u2} α β m f F)) s) (Set.image.{u3, u1} α β m (CFilter.f.{u3, u2} (Set.{u3} α) (Filter.Realizer.σ.{u3, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} α) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} α) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} α) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} α) (Set.instCompleteBooleanAlgebraSet.{u3} α)))))) (Filter.Realizer.F.{u3, u2} α f F) s))
Case conversion may be inaccurate. Consider using '#align filter.realizer.map_F Filter.Realizer.map_Fₓ'. -/
@[simp]
theorem map_F (m : α → β) {f : Filter α} (F : f.Realizer) (s) : (F.map m).f s = image m (F.f s) :=
  rfl
#align filter.realizer.map_F Filter.Realizer.map_F

#print Filter.Realizer.comap /-
/-- Construct a realizer for `comap m f` given a realizer for `f` -/
protected def comap (m : α → β) {f : Filter β} (F : f.Realizer) : (comap m f).Realizer :=
  ⟨F.σ,
    { f := fun s => preimage m (F.f s)
      pt := F.f.pt
      inf := F.f.inf
      inf_le_left := fun a b => preimage_mono (F.f.inf_le_left _ _)
      inf_le_right := fun a b => preimage_mono (F.f.inf_le_right _ _) },
    filter_eq <|
      Set.ext fun x => by
        cases F <;> subst f <;> simp [CFilter.toFilter, mem_comap] <;>
          exact
            ⟨fun ⟨s, h⟩ => ⟨_, ⟨s, subset.refl _⟩, h⟩, fun ⟨y, ⟨s, h⟩, h₂⟩ =>
              ⟨s, subset.trans (preimage_mono h) h₂⟩⟩⟩
#align filter.realizer.comap Filter.Realizer.comap
-/

/- warning: filter.realizer.sup -> Filter.Realizer.sup is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {f : Filter.{u1} α} {g : Filter.{u1} α}, (Filter.Realizer.{u1, u2} α f) -> (Filter.Realizer.{u1, u3} α g) -> (Filter.Realizer.{u1, max u2 u3} α (Sup.sup.{u1} (Filter.{u1} α) (SemilatticeSup.toHasSup.{u1} (Filter.{u1} α) (Lattice.toSemilatticeSup.{u1} (Filter.{u1} α) (ConditionallyCompleteLattice.toLattice.{u1} (Filter.{u1} α) (CompleteLattice.toConditionallyCompleteLattice.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α))))) f g))
but is expected to have type
  forall {α : Type.{u1}} {f : Filter.{u1} α} {g : Filter.{u1} α}, (Filter.Realizer.{u1, u2} α f) -> (Filter.Realizer.{u1, u3} α g) -> (Filter.Realizer.{u1, max u3 u2} α (Sup.sup.{u1} (Filter.{u1} α) (SemilatticeSup.toSup.{u1} (Filter.{u1} α) (Lattice.toSemilatticeSup.{u1} (Filter.{u1} α) (ConditionallyCompleteLattice.toLattice.{u1} (Filter.{u1} α) (CompleteLattice.toConditionallyCompleteLattice.{u1} (Filter.{u1} α) (Filter.instCompleteLatticeFilter.{u1} α))))) f g))
Case conversion may be inaccurate. Consider using '#align filter.realizer.sup Filter.Realizer.supₓ'. -/
/-- Construct a realizer for the sup of two filters -/
protected def sup {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f ⊔ g).Realizer :=
  ⟨F.σ × G.σ,
    { f := fun ⟨s, t⟩ => F.f s ∪ G.f t
      pt := (F.f.pt, G.f.pt)
      inf := fun ⟨a, a'⟩ ⟨b, b'⟩ => (F.f.inf a b, G.f.inf a' b')
      inf_le_left := fun ⟨a, a'⟩ ⟨b, b'⟩ =>
        union_subset_union (F.f.inf_le_left _ _) (G.f.inf_le_left _ _)
      inf_le_right := fun ⟨a, a'⟩ ⟨b, b'⟩ =>
        union_subset_union (F.f.inf_le_right _ _) (G.f.inf_le_right _ _) },
    filter_eq <|
      Set.ext fun x => by
        cases F <;> cases G <;> substs f g <;> simp [CFilter.toFilter] <;>
          exact
            ⟨fun ⟨s, t, h⟩ =>
              ⟨⟨s, subset.trans (subset_union_left _ _) h⟩,
                ⟨t, subset.trans (subset_union_right _ _) h⟩⟩,
              fun ⟨⟨s, h₁⟩, ⟨t, h₂⟩⟩ => ⟨s, t, union_subset h₁ h₂⟩⟩⟩
#align filter.realizer.sup Filter.Realizer.sup

/- warning: filter.realizer.inf -> Filter.Realizer.inf is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {f : Filter.{u1} α} {g : Filter.{u1} α}, (Filter.Realizer.{u1, u2} α f) -> (Filter.Realizer.{u1, u3} α g) -> (Filter.Realizer.{u1, max u2 u3} α (Inf.inf.{u1} (Filter.{u1} α) (Filter.hasInf.{u1} α) f g))
but is expected to have type
  forall {α : Type.{u1}} {f : Filter.{u1} α} {g : Filter.{u1} α}, (Filter.Realizer.{u1, u2} α f) -> (Filter.Realizer.{u1, u3} α g) -> (Filter.Realizer.{u1, max u3 u2} α (Inf.inf.{u1} (Filter.{u1} α) (Filter.instInfFilter.{u1} α) f g))
Case conversion may be inaccurate. Consider using '#align filter.realizer.inf Filter.Realizer.infₓ'. -/
/-- Construct a realizer for the inf of two filters -/
protected def inf {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f ⊓ g).Realizer :=
  ⟨F.σ × G.σ,
    { f := fun ⟨s, t⟩ => F.f s ∩ G.f t
      pt := (F.f.pt, G.f.pt)
      inf := fun ⟨a, a'⟩ ⟨b, b'⟩ => (F.f.inf a b, G.f.inf a' b')
      inf_le_left := fun ⟨a, a'⟩ ⟨b, b'⟩ =>
        inter_subset_inter (F.f.inf_le_left _ _) (G.f.inf_le_left _ _)
      inf_le_right := fun ⟨a, a'⟩ ⟨b, b'⟩ =>
        inter_subset_inter (F.f.inf_le_right _ _) (G.f.inf_le_right _ _) },
    by
    ext x
    cases F <;> cases G <;> substs f g <;> simp [CFilter.toFilter]
    constructor
    · rintro ⟨s : F_σ, t : G_σ, h⟩
      apply mem_inf_of_inter _ _ h
      use s
      use t
    · rintro ⟨s, ⟨a, ha⟩, t, ⟨b, hb⟩, rfl⟩
      exact ⟨a, b, inter_subset_inter ha hb⟩⟩
#align filter.realizer.inf Filter.Realizer.inf

#print Filter.Realizer.cofinite /-
/-- Construct a realizer for the cofinite filter -/
protected def cofinite [DecidableEq α] : (@cofinite α).Realizer :=
  ⟨Finset α,
    { f := fun s => { a | a ∉ s }
      pt := ∅
      inf := (· ∪ ·)
      inf_le_left := fun s t a => mt (Finset.mem_union_left _)
      inf_le_right := fun s t a => mt (Finset.mem_union_right _) },
    filter_eq <|
      Set.ext fun x =>
        ⟨fun ⟨s, h⟩ => s.finite_toSet.Subset (compl_subset_comm.1 h), fun h =>
          ⟨h.toFinset, by simp⟩⟩⟩
#align filter.realizer.cofinite Filter.Realizer.cofinite
-/

#print Filter.Realizer.bind /-
/-- Construct a realizer for filter bind -/
protected def bind {f : Filter α} {m : α → Filter β} (F : f.Realizer) (G : ∀ i, (m i).Realizer) :
    (f.bind m).Realizer :=
  ⟨Σs : F.σ, ∀ i ∈ F.f s, (G i).σ,
    { f := fun ⟨s, f⟩ => ⋃ i ∈ F.f s, (G i).f (f i H)
      pt := ⟨F.f.pt, fun i H => (G i).f.pt⟩
      inf := fun ⟨a, f⟩ ⟨b, f'⟩ =>
        ⟨F.f.inf a b, fun i h =>
          (G i).f.inf (f i (F.f.inf_le_left _ _ h)) (f' i (F.f.inf_le_right _ _ h))⟩
      inf_le_left := fun ⟨a, f⟩ ⟨b, f'⟩ x =>
        show
          (x ∈ ⋃ (i : α) (H : i ∈ F.f (F.f.inf a b)), _) →
            x ∈ ⋃ (i) (H : i ∈ F.f a), (G i).f (f i H)
          by simp <;> exact fun i h₁ h₂ => ⟨i, F.F.inf_le_left _ _ h₁, (G i).f.inf_le_left _ _ h₂⟩
      inf_le_right := fun ⟨a, f⟩ ⟨b, f'⟩ x =>
        show
          (x ∈ ⋃ (i : α) (H : i ∈ F.f (F.f.inf a b)), _) →
            x ∈ ⋃ (i) (H : i ∈ F.f b), (G i).f (f' i H)
          by
          simp <;> exact fun i h₁ h₂ => ⟨i, F.F.inf_le_right _ _ h₁, (G i).f.inf_le_right _ _ h₂⟩ },
    filter_eq <|
      Set.ext fun x => by
        cases' F with _ F _ <;> subst f <;> simp [CFilter.toFilter, mem_bind] <;>
          exact
            ⟨fun ⟨s, f, h⟩ =>
              ⟨F s, ⟨s, subset.refl _⟩, fun i H =>
                (G i).mem_sets.2 ⟨f i H, fun a h' => h ⟨_, ⟨i, rfl⟩, _, ⟨H, rfl⟩, h'⟩⟩⟩,
              fun ⟨y, ⟨s, h⟩, f⟩ =>
              let ⟨f', h'⟩ :=
                Classical.axiom_of_choice fun i : F s => (G i).mem_sets.1 (f i (h i.2))
              ⟨s, fun i h => f' ⟨i, h⟩, fun a ⟨_, ⟨i, rfl⟩, _, ⟨H, rfl⟩, m⟩ => h' ⟨_, H⟩ m⟩⟩⟩
#align filter.realizer.bind Filter.Realizer.bind
-/

/-- Construct a realizer for indexed supremum -/
protected def supᵢ {f : α → Filter β} (F : ∀ i, (f i).Realizer) : (⨆ i, f i).Realizer :=
  let F' : (⨆ i, f i).Realizer :=
    (Realizer.bind Realizer.top F).of_eq <|
      filter_eq <| Set.ext <| by simp [Filter.bind, eq_univ_iff_forall, supr_sets_eq]
  F'.of_equiv <|
    show (Σu : Unit, ∀ i : α, True → (F i).σ) ≃ ∀ i, (F i).σ from
      ⟨fun ⟨_, f⟩ i => f i ⟨⟩, fun f => ⟨(), fun i _ => f i⟩, fun ⟨⟨⟩, f⟩ => by
        dsimp <;> congr <;> simp, fun f => rfl⟩
#align filter.realizer.Sup Filter.Realizer.supᵢₓ

#print Filter.Realizer.prod /-
/-- Construct a realizer for the product of filters -/
protected def prod {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f.Prod g).Realizer :=
  (F.comap _).inf (G.comap _)
#align filter.realizer.prod Filter.Realizer.prod
-/

/- warning: filter.realizer.le_iff -> Filter.Realizer.le_iff is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {f : Filter.{u1} α} {g : Filter.{u1} α} (F : Filter.Realizer.{u1, u2} α f) (G : Filter.Realizer.{u1, u3} α g), Iff (LE.le.{u1} (Filter.{u1} α) (Preorder.toLE.{u1} (Filter.{u1} α) (PartialOrder.toPreorder.{u1} (Filter.{u1} α) (Filter.partialOrder.{u1} α))) f g) (forall (b : Filter.Realizer.σ.{u1, u3} α g G), Exists.{succ u2} (Filter.Realizer.σ.{u1, u2} α f F) (fun (a : Filter.Realizer.σ.{u1, u2} α f F) => LE.le.{u1} (Set.{u1} α) (Set.hasLe.{u1} α) (coeFn.{max (succ u1) (succ u2), max (succ u2) (succ u1)} (CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u2} α f F) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u2} α f F) a) (coeFn.{max (succ u1) (succ u3), max (succ u3) (succ u1)} (CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α g G) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α g G) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u3} α g G) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α g G) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u3} α g G) b)))
but is expected to have type
  forall {α : Type.{u3}} {f : Filter.{u3} α} {g : Filter.{u3} α} (F : Filter.Realizer.{u3, u2} α f) (G : Filter.Realizer.{u3, u1} α g), Iff (LE.le.{u3} (Filter.{u3} α) (Preorder.toLE.{u3} (Filter.{u3} α) (PartialOrder.toPreorder.{u3} (Filter.{u3} α) (Filter.instPartialOrderFilter.{u3} α))) f g) (forall (b : Filter.Realizer.σ.{u3, u1} α g G), Exists.{succ u2} (Filter.Realizer.σ.{u3, u2} α f F) (fun (a : Filter.Realizer.σ.{u3, u2} α f F) => LE.le.{u3} (Set.{u3} α) (Set.instLESet.{u3} α) (CFilter.f.{u3, u2} (Set.{u3} α) (Filter.Realizer.σ.{u3, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} α) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} α) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} α) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} α) (Set.instCompleteBooleanAlgebraSet.{u3} α)))))) (Filter.Realizer.F.{u3, u2} α f F) a) (CFilter.f.{u3, u1} (Set.{u3} α) (Filter.Realizer.σ.{u3, u1} α g G) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} α) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} α) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} α) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} α) (Set.instCompleteBooleanAlgebraSet.{u3} α)))))) (Filter.Realizer.F.{u3, u1} α g G) b)))
Case conversion may be inaccurate. Consider using '#align filter.realizer.le_iff Filter.Realizer.le_iffₓ'. -/
theorem le_iff {f g : Filter α} (F : f.Realizer) (G : g.Realizer) :
    f ≤ g ↔ ∀ b : G.σ, ∃ a : F.σ, F.f a ≤ G.f b :=
  ⟨fun H t => F.mem_sets.1 (H (G.mem_sets.2 ⟨t, Subset.refl _⟩)), fun H x h =>
    F.mem_sets.2 <|
      let ⟨s, h₁⟩ := G.mem_sets.1 h
      let ⟨t, h₂⟩ := H s
      ⟨t, Subset.trans h₂ h₁⟩⟩
#align filter.realizer.le_iff Filter.Realizer.le_iff

/- warning: filter.realizer.tendsto_iff -> Filter.Realizer.tendsto_iff is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {β : Type.{u2}} (f : α -> β) {l₁ : Filter.{u1} α} {l₂ : Filter.{u2} β} (L₁ : Filter.Realizer.{u1, u3} α l₁) (L₂ : Filter.Realizer.{u2, u4} β l₂), Iff (Filter.Tendsto.{u1, u2} α β f l₁ l₂) (forall (b : Filter.Realizer.σ.{u2, u4} β l₂ L₂), Exists.{succ u3} (Filter.Realizer.σ.{u1, u3} α l₁ L₁) (fun (a : Filter.Realizer.σ.{u1, u3} α l₁ L₁) => forall (x : α), (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x (coeFn.{max (succ u1) (succ u3), max (succ u3) (succ u1)} (CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α l₁ L₁) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α l₁ L₁) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u3} α l₁ L₁) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u3} (Set.{u1} α) (Filter.Realizer.σ.{u1, u3} α l₁ L₁) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u3} α l₁ L₁) a)) -> (Membership.Mem.{u2, u2} β (Set.{u2} β) (Set.hasMem.{u2} β) (f x) (coeFn.{max (succ u2) (succ u4), max (succ u4) (succ u2)} (CFilter.{u2, u4} (Set.{u2} β) (Filter.Realizer.σ.{u2, u4} β l₂ L₂) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} β) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} β) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} β) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} β) (Set.completeBooleanAlgebra.{u2} β))))))) (fun (_x : CFilter.{u2, u4} (Set.{u2} β) (Filter.Realizer.σ.{u2, u4} β l₂ L₂) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} β) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} β) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} β) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} β) (Set.completeBooleanAlgebra.{u2} β))))))) => (Filter.Realizer.σ.{u2, u4} β l₂ L₂) -> (Set.{u2} β)) (CFilter.hasCoeToFun.{u2, u4} (Set.{u2} β) (Filter.Realizer.σ.{u2, u4} β l₂ L₂) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} β) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} β) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} β) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} β) (Set.completeBooleanAlgebra.{u2} β))))))) (Filter.Realizer.f.{u2, u4} β l₂ L₂) b))))
but is expected to have type
  forall {α : Type.{u4}} {β : Type.{u3}} (f : α -> β) {l₁ : Filter.{u4} α} {l₂ : Filter.{u3} β} (L₁ : Filter.Realizer.{u4, u2} α l₁) (L₂ : Filter.Realizer.{u3, u1} β l₂), Iff (Filter.Tendsto.{u4, u3} α β f l₁ l₂) (forall (b : Filter.Realizer.σ.{u3, u1} β l₂ L₂), Exists.{succ u2} (Filter.Realizer.σ.{u4, u2} α l₁ L₁) (fun (a : Filter.Realizer.σ.{u4, u2} α l₁ L₁) => forall (x : α), (Membership.mem.{u4, u4} α (Set.{u4} α) (Set.instMembershipSet.{u4} α) x (CFilter.f.{u4, u2} (Set.{u4} α) (Filter.Realizer.σ.{u4, u2} α l₁ L₁) (CompleteSemilatticeInf.toPartialOrder.{u4} (Set.{u4} α) (CompleteLattice.toCompleteSemilatticeInf.{u4} (Set.{u4} α) (Order.Coframe.toCompleteLattice.{u4} (Set.{u4} α) (CompleteDistribLattice.toCoframe.{u4} (Set.{u4} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u4} (Set.{u4} α) (Set.instCompleteBooleanAlgebraSet.{u4} α)))))) (Filter.Realizer.F.{u4, u2} α l₁ L₁) a)) -> (Membership.mem.{u3, u3} β (Set.{u3} β) (Set.instMembershipSet.{u3} β) (f x) (CFilter.f.{u3, u1} (Set.{u3} β) (Filter.Realizer.σ.{u3, u1} β l₂ L₂) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} β) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} β) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} β) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} β) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} β) (Set.instCompleteBooleanAlgebraSet.{u3} β)))))) (Filter.Realizer.F.{u3, u1} β l₂ L₂) b))))
Case conversion may be inaccurate. Consider using '#align filter.realizer.tendsto_iff Filter.Realizer.tendsto_iffₓ'. -/
theorem tendsto_iff (f : α → β) {l₁ : Filter α} {l₂ : Filter β} (L₁ : l₁.Realizer)
    (L₂ : l₂.Realizer) : Tendsto f l₁ l₂ ↔ ∀ b, ∃ a, ∀ x ∈ L₁.f a, f x ∈ L₂.f b :=
  (le_iff (L₁.map f) L₂).trans <| forall_congr' fun b => exists_congr fun a => image_subset_iff
#align filter.realizer.tendsto_iff Filter.Realizer.tendsto_iff

/- warning: filter.realizer.ne_bot_iff -> Filter.Realizer.ne_bot_iff is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {f : Filter.{u1} α} (F : Filter.Realizer.{u1, u2} α f), Iff (Ne.{succ u1} (Filter.{u1} α) f (Bot.bot.{u1} (Filter.{u1} α) (CompleteLattice.toHasBot.{u1} (Filter.{u1} α) (Filter.completeLattice.{u1} α)))) (forall (a : Filter.Realizer.σ.{u1, u2} α f F), Set.Nonempty.{u1} α (coeFn.{max (succ u1) (succ u2), max (succ u2) (succ u1)} (CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (fun (_x : CFilter.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) => (Filter.Realizer.σ.{u1, u2} α f F) -> (Set.{u1} α)) (CFilter.hasCoeToFun.{u1, u2} (Set.{u1} α) (Filter.Realizer.σ.{u1, u2} α f F) (CompleteSemilatticeInf.toPartialOrder.{u1} (Set.{u1} α) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Set.{u1} α) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} α) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} α) (Set.completeBooleanAlgebra.{u1} α))))))) (Filter.Realizer.f.{u1, u2} α f F) a))
but is expected to have type
  forall {α : Type.{u2}} {f : Filter.{u2} α} (F : Filter.Realizer.{u2, u1} α f), Iff (Ne.{succ u2} (Filter.{u2} α) f (Bot.bot.{u2} (Filter.{u2} α) (CompleteLattice.toBot.{u2} (Filter.{u2} α) (Filter.instCompleteLatticeFilter.{u2} α)))) (forall (a : Filter.Realizer.σ.{u2, u1} α f F), Set.Nonempty.{u2} α (CFilter.f.{u2, u1} (Set.{u2} α) (Filter.Realizer.σ.{u2, u1} α f F) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} α) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} α) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} α) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} α) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} α) (Set.instCompleteBooleanAlgebraSet.{u2} α)))))) (Filter.Realizer.F.{u2, u1} α f F) a))
Case conversion may be inaccurate. Consider using '#align filter.realizer.ne_bot_iff Filter.Realizer.ne_bot_iffₓ'. -/
theorem ne_bot_iff {f : Filter α} (F : f.Realizer) : f ≠ ⊥ ↔ ∀ a : F.σ, (F.f a).Nonempty := by
  classical
    rw [not_iff_comm, ← le_bot_iff, F.le_iff realizer.bot, not_forall]
    simp only [Set.not_nonempty_iff_eq_empty]
    exact
      ⟨fun ⟨x, e⟩ _ => ⟨x, le_of_eq e⟩, fun h =>
        let ⟨x, h⟩ := h ()
        ⟨x, le_bot_iff.1 h⟩⟩
#align filter.realizer.ne_bot_iff Filter.Realizer.ne_bot_iff

end Filter.Realizer

author: leanprover-community


text:
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
-/
import tactic.hint

namespace tactic

open expr
open tactic.interactive ( casesm constructor_matching )

/--
  find all assumptions of the shape `¬ (p ∧ q)` or `¬ (p ∨ q)` and
  replace them using de Morgan's law.
-/
meta def distrib_not : tactic unit :=
do hs ← local_context,
   hs.for_each $ λ h,
    all_goals' $
    iterate_at_most' 3 $
      do h ← get_local h.local_pp_name,
         e ← infer_type h,
         match e with
         | `(¬ _ = _)   := replace h.local_pp_name ``(mt iff.to_eq %%h)
         | `(_ ≠ _)     := replace h.local_pp_name ``(mt iff.to_eq %%h)
         | `(_ = _)     := replace h.local_pp_name ``(eq.to_iff %%h)
         | `(¬ (_ ∧ _)) := replace h.local_pp_name ``(decidable.not_and_distrib'.mp %%h) <|>
                           replace h.local_pp_name ``(decidable.not_and_distrib.mp %%h)
         | `(¬ (_ ∨ _)) := replace h.local_pp_name ``(not_or_distrib.mp %%h)
         | `(¬ _ ≠ _)   := replace h.local_pp_name ``(decidable.of_not_not %%h)
         | `(¬ ¬ _)     := replace h.local_pp_name ``(decidable.of_not_not %%h)
         | `(¬ (_ → (_ : Prop))) := replace h.local_pp_name ``(decidable.not_imp.mp %%h)
         | `(¬ (_ ↔ _)) := replace h.local_pp_name ``(decidable.not_iff.mp %%h)
         | `(_ ↔ _) := replace h.local_pp_name ``(decidable.iff_iff_and_or_not_and_not.mp %%h) <|>
                       replace h.local_pp_name
                         ``(decidable.iff_iff_and_or_not_and_not.mp (%%h).symm) <|>
                       () <$ tactic.cases h
         | `(_ → _)     := replace h.local_pp_name ``(decidable.not_or_of_imp %%h)
         | _ := failed
         end

/-!
  The following definitions maintain a path compression datastructure, i.e. a forest such that:
    - every node is the type of a hypothesis
    - there is a edge between two nodes only if they are provably equivalent
    - every edge is labelled with a proof of equivalence for its vertices
    - edges are added when normalizing propositions.
-/

meta def tauto_state := ref $ expr_map (option (expr × expr))

meta def modify_ref {α : Type} (r : ref α) (f : α → α) :=
read_ref r >>= write_ref r ∘ f

meta def add_refl (r : tauto_state) (e : expr) : tactic (expr × expr) :=
do m ← read_ref r,
   p ← mk_mapp `rfl [none,e],
   write_ref r $ m.insert e none,
   return (e,p)

/--
  If there exists a symmetry lemma that can be applied to the hypothesis `e`,
  store it.
-/
meta def add_symm_proof (r : tauto_state) (e : expr) : tactic (expr × expr) :=
do env ← get_env,
   let rel := e.get_app_fn.const_name,
   some symm ← pure $ environment.symm_for env rel
     | add_refl r e,
   (do e' ← mk_meta_var `(Prop),
       iff_t ← to_expr ``(%%e = %%e'),
       (_,p) ← solve_aux iff_t
         (applyc `iff.to_eq ; () <$ split ; applyc symm),
       e' ← instantiate_mvars e',
       m ← read_ref r,
       write_ref r $ (m.insert e (e',p)).insert e' none,
       return (e',p) )
   <|> add_refl r e

meta def add_edge (r : tauto_state) (x y p : expr) : tactic unit :=
modify_ref r $ λ m, m.insert x (y,p)

/--
  Retrieve the root of the hypothesis `e` from the proof forest.
  If `e` has not been internalized, add it to the proof forest.
-/
meta def root (r : tauto_state) : expr → tactic (expr × expr) | e :=
do m ← read_ref r,
   let record_e : tactic (expr × expr) :=
       match e with
       | v@(expr.mvar _ _ _) :=
         (do (e,p) ← get_assignment v >>= root,
             add_edge r v e p,
             return (e,p)) <|>
         add_refl r e
       | _ := add_refl r e
       end,
   some e' ← pure $ m.find e | record_e,
   match e' with
   | (some (e',p')) :=
     do (e'',p'') ← root e',
        p'' ← mk_app `eq.trans [p',p''],
        add_edge r e e'' p'',
        pure (e'',p'')
   | none := prod.mk e <$> mk_mapp `rfl [none,some e]
   end

/--
  Given hypotheses `a` and `b`, build a proof that `a` is equivalent to `b`,
  applying congruence and recursing into arguments if `a` and `b`
  are applications of function symbols.
-/
meta def symm_eq (r : tauto_state) : expr → expr → tactic expr | a b :=
do m ← read_ref r,
   (a',pa) ← root r a,
   (b',pb) ← root r b,
   (unify a' b' >> add_refl r a' *> mk_mapp `rfl [none,a]) <|>
    do p ← match (a', b') with
           | (`(¬ %%a₀), `(¬ %%b₀)) :=
             do p  ← symm_eq a₀ b₀,
                p' ← mk_app `congr_arg [`(not),p],
                add_edge r a' b' p',
                return p'
           | (`(%%a₀ ∧ %%a₁), `(%%b₀ ∧ %%b₁)) :=
             do p₀ ← symm_eq a₀ b₀,
                p₁ ← symm_eq a₁ b₁,
                p' ← to_expr ``(congr (congr_arg and %%p₀) %%p₁),
                add_edge r a' b' p',
                return p'
           | (`(%%a₀ ∨ %%a₁), `(%%b₀ ∨ %%b₁)) :=
             do p₀ ← symm_eq a₀ b₀,
                p₁ ← symm_eq a₁ b₁,
                p' ← to_expr ``(congr (congr_arg or %%p₀) %%p₁),
                add_edge r a' b' p',
                return p'
           | (`(%%a₀ ↔ %%a₁), `(%%b₀ ↔ %%b₁)) :=
             (do p₀ ← symm_eq a₀ b₀,
                 p₁ ← symm_eq a₁ b₁,
                 p' ← to_expr ``(congr (congr_arg iff %%p₀) %%p₁),
                 add_edge r a' b' p',
                 return p') <|>
             do p₀ ← symm_eq a₀ b₁,
                p₁ ← symm_eq a₁ b₀,
                p' ← to_expr ``(eq.trans (congr (congr_arg iff %%p₀) %%p₁)
                                         (iff.to_eq iff.comm ) ),
                add_edge r a' b' p',
                return p'
           | (`(%%a₀ → %%a₁), `(%%b₀ → %%b₁)) :=
             if ¬ a₁.has_var ∧ ¬ b₁.has_var then
             do p₀ ← symm_eq a₀ b₀,
                p₁ ← symm_eq a₁ b₁,
                p' ← mk_app `congr_arg [`(implies),p₀,p₁],
                add_edge r a' b' p',
                return p'
             else unify a' b' >> add_refl r a' *> mk_mapp `rfl [none,a]
           | (_, _) :=
             (do guard $ a'.get_app_fn.is_constant ∧
                         a'.get_app_fn.const_name = b'.get_app_fn.const_name,
                 (a'',pa') ← add_symm_proof r a',
                 guard $ a'' =ₐ b',
                 pure pa' )
           end,
    p' ← mk_eq_trans pa p,
    add_edge r a' b' p',
    mk_eq_symm pb >>= mk_eq_trans p'

meta def find_eq_type (r : tauto_state) : expr → list expr → tactic (expr × expr)
| e []         := failed
| e (H :: Hs) :=
  do t  ← infer_type H,
     (prod.mk H <$> symm_eq r e t) <|> find_eq_type e Hs

private meta def contra_p_not_p (r : tauto_state) : list expr → list expr → tactic unit
| []         Hs := failed
| (H1 :: Rs) Hs :=
  do t ← (extract_opt_auto_param <$> infer_type H1) >>= whnf,
     (do a   ← match_not t,
         (H2,p)  ← find_eq_type r a Hs,
         H2 ← to_expr ``( (%%p).mpr %%H2 ),
         tgt ← target,
         pr  ← mk_app `absurd [tgt, H2, H1],
         tactic.exact pr)
     <|> contra_p_not_p Rs Hs

meta def contradiction_with (r : tauto_state) : tactic unit :=
contradiction <|>
do tactic.try intro1,
   ctx ← local_context,
   contra_p_not_p r ctx ctx

meta def contradiction_symm :=
using_new_ref (native.rb_map.mk _ _) contradiction_with

meta def assumption_with (r : tauto_state) : tactic unit :=
do { ctx ← local_context,
     t   ← target,
     (H,p) ← find_eq_type r t ctx,
     mk_eq_mpr p H >>= tactic.exact }
<|> fail "assumption tactic failed"

meta def assumption_symm :=
using_new_ref (native.rb_map.mk _ _) assumption_with

/--
  Configuration options for `tauto`.
  If `classical` is `tt`, runs `classical` before the rest of `tauto`.
  `closer` is run on any remaining subgoals left by `tauto_core; basic_tauto_tacs`.
-/
meta structure tauto_cfg :=
(classical : bool     := ff)
(closer : tactic unit := pure ())

meta def tautology (cfg : tauto_cfg := {}) : tactic unit := focus1 $
  let basic_tauto_tacs : list (tactic unit) :=
        [reflexivity, solve_by_elim,
          constructor_matching none [``(_ ∧ _),``(_ ↔ _),``(Exists _),``(true)]],

      tauto_core (r : tauto_state) : tactic unit :=
        do try (contradiction_with r);
           try (assumption_with r);
           repeat (do
             gs ← get_goals,
             repeat (() <$ tactic.intro1);
             distrib_not;
             casesm (some ()) [``(_ ∧ _),``(_ ∨ _),``(Exists _),``(false)];
             try (contradiction_with r);
             try (target >>= match_or >> refine ``( or_iff_not_imp_left.mpr _));
             try (target >>= match_or >> refine ``( or_iff_not_imp_right.mpr _));
             repeat (() <$ tactic.intro1);
             constructor_matching (some ()) [``(_ ∧ _),``(_ ↔ _),``(true)];
             try (assumption_with r),
             gs' ← get_goals,
             guard (gs ≠ gs') ) in

    do when cfg.classical (classical tt),
       using_new_ref (expr_map.mk _) tauto_core;
       repeat (first basic_tauto_tacs); cfg.closer, done

namespace interactive
local postfix (name := parser.optional) `?`:9001 := optional
setup_tactic_parser

/--
`tautology` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `reflexivity` or `solve_by_elim`.
This is a finishing tactic: it either closes the goal or raises an error.
The variant `tautology!` uses the law of excluded middle.

`tautology {closer := tac}` will use `tac` on any subgoals created by `tautology`
that it is unable to solve before failing.
-/
meta def tautology (c : parse $ (tk "!")?) (cfg : tactic.tauto_cfg := {}) :=
tactic.tautology $ { classical := c.is_some, ..cfg }

-- Now define a shorter name for the tactic `tautology`.

/--
`tauto` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `reflexivity` or `solve_by_elim`.
This is a finishing tactic: it either closes the goal or raises an error.
The variant `tauto!` uses the law of excluded middle.

`tauto {closer := tac}` will use `tac` on any subgoals created by `tauto`
that it is unable to solve before failing.
-/
meta def tauto (c : parse $ (tk "!")?) (cfg : tactic.tauto_cfg := {}) : tactic unit :=
tautology c cfg

add_hint_tactic "tauto"

/--
This tactic (with shorthand `tauto`) breaks down assumptions of the form
`_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `reflexivity` or `solve_by_elim`. This is a finishing tactic: it
either closes the goal or raises an error.

The variants `tautology!` and `tauto!` use the law of excluded middle.

For instance, one can write:
```lean
example (p q r : Prop) [decidable p] [decidable r] : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by tauto
```
and the decidability assumptions can be dropped if `tauto!` is used
instead of `tauto`.

`tauto {closer := tac}` will use `tac` on any subgoals created by `tauto`
that it is unable to solve before failing.
-/
add_tactic_doc
{ name       := "tautology",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.tautology, `tactic.interactive.tauto],
  tags       := ["logic", "decision procedure"] }

end interactive
end tactic

repo: mathlib


import combinatorics.simple_graph.coloring

--OUTPUT 1
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  split,
  { assume H : G.colorable 2,
    let f : V → fin 2 := coloring H,
    have h1 : (fintype.elems (finset.range 2)) = ({0, 1} : multiset ℕ), from sorry,
    have h2 : (fintype.elems (finset.range 2)) ∈ ({0, 1} : multiset ℕ), from sorry,

    have h3 : ∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B), from sorry,
    show ∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B), from sorry,
  },
  { assume H : (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)),
    sorry,
  },
end

--OUTPUT 2
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  split;
  assume (h : G.colorable 2),
  {
    sorry,
  },
  {
    assume (h : ∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)),
    sorry,
  },
end

--OUTPUT 3
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  have h1 : (G.colorable 2) → (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)), from sorry,
  have h2 : (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) → (G.colorable 2), from sorry,
  have h3 : ((G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B))), from sorry,
  show (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)), from h3,
end

--OUTPUT 4
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  split,
  {
    assume h1 : (G.colorable 2),
    show ∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B), from sorry,
  },
  {
    assume h2 : (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)),
    show G.colorable 2, from sorry,
  }
end

--OUTPUT 5
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  split,
  { assume hf : G.colorable 2,
    obtain ⟨f, hf1, hf2⟩ := hf, -- the 2-colorable structure, f
    have hf3 : ((f ⁻¹' {0}) ⊕ (f ⁻¹' {1})) = V, from sorry,

    -- first, we show that G is a subgraph of (f ⁻¹' {0}) ⋃ (f ⁻¹' {1}).
    -- then we will show that the subgraph is complete bipartite graph.
    have hG : G ≤ cast (congr_arg _ hf3) (complete_bipartite_graph (f ⁻¹' {0}) (f ⁻¹' {1})), from sorry,
    use (f ⁻¹' {0}),
    use (f ⁻¹' {1}),
    use hf3,
    show G ≤ cast (congr_arg _ hf3) (complete_bipartite_graph (f ⁻¹' {0}) (f ⁻¹' {1})), from hG,
  },
  { assume hf : (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)),
    have h1 : ∃ f : G.V → fin 2, (eq.rec_on (some hf).2.2) ∘ f = some hf ∘ G.V.to_equiv, from sorry,
    have h2 : ∀ v w : G.V, G.adj v w → f v ≠ f w, from sorry,
    -- construct the 2-colorable structure
    have h3 : (eq.rec_on (some hf).2.2) ∘ f = some hf ∘ G.V.to_equiv, from sorry,
    let f' := @simple_graph.two_colorable_structure.mk G f (h1.fst) (h2) (h3),
    have h4 : G.colorable 2, from sorry,
    show (G.colorable 2), from sorry,
  }
end

--OUTPUT 6
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  split,
  assume gc2 : G.colorable 2,

  have gc2_coloring : ∀ (f : (Π (v : V), fin 2)), G.is_coloring f, from sorry,
  have h0 : ∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B), from sorry,

  show (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)), from sorry,

  assume h0 : ∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B),
  have gcb : ∃ (f : (Π (v : V), fin 2)), G.is_coloring f, from sorry,

  show G.colorable 2, from sorry,
end

--OUTPUT 7
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  split,
  {
    assume h, sorry
  },
  {
    assume ⟨A, B, h⟩, sorry
  }
end

--OUTPUT 8
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  show (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)), from sorry
end

--OUTPUT 9
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) := sorry

end

--OUTPUT 10
theorem bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
begin
  sorry,
end

/- FEW SHOT PROMPTS TO CODEX(START)
/--`theorem`
Power Set is Closed under Intersection
Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:
:$\forall A, B \in \powerset S: A \cap B \in \powerset S$
`proof`
Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.
{{qed}}
-/
theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈ 𝒫 S, (A ∩ B) ∈ 𝒫 S :=
begin
  assume (A : set α) (hA : A ∈ 𝒫 S) (B : set α) (hB : B ∈ 𝒫 S),
  have h1 : (A ⊆ S) ∧ (B ⊆ S), from sorry,
  have h2 : (A ∩ B) ⊆ A, from sorry,
  have h3 : (A ∩ B) ⊆ S, from sorry,
  show (A ∩ B) ∈  𝒫 S, from sorry,
end

/--`theorem`
Square of Sum
 :$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$
`proof`
Follows from the distribution of multiplication over addition:

{{begin-eqn}}
{{eqn | l = \left({x + y}\right)^2
      | r = \left({x + y}\right) \cdot \left({x + y}\right)
}}
{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x^2 + 2xy + y^2
      | c =
}}
{{end-eqn}}
{{qed}}
-/
theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2) :=
begin
  calc (x + y)^2 = (x+y)*(x+y) : by sorry
  ... = x*(x+y) + y*(x+y) : by sorry
  ... = x*x + x*y + y*x + y*y : by sorry
  ... = x^2 + 2*x*y + y^2 : by sorry,
end

/--`theorem`
Identity of Group is Unique
Let $\struct {G, \circ}$ be a group. Then there is a unique identity element $e \in G$.
`proof`
From Group has Latin Square Property, there exists a unique $x \in G$ such that:
:$a x = b$

and there exists a unique $y \in G$ such that:
:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:
:$a x = a$

and there exists a unique $y \in G$ such that:
:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.
{{qed}}
-/
theorem group_identity_unique {G : Type*} [group G] : ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a :=
begin
  have h1 : ∀ a b : G, ∃! x : G, a * x = b, from sorry,
  have h2 : ∀ a b : G, ∃! y : G, y * a = b, from sorry,

  have h3 : ∀ a : G, ∃! x : G, a * x = a, from sorry,
  have h4 : ∀ a : G, ∃! y : G, y * a = a, from sorry,

  have h5 : ∀ a : G, classical.some (h3 a) = (1 : G), from sorry,
  have h6 : ∀ a : G, classical.some (h4 a) = (1 : G), from sorry,

  show ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a, from by {
    use (1 : G),
    have h7 : ∀ e : G, (∀ a : G, e * a = a ∧ a * e = a) → e = 1, from by {
      assume (e : G) (h7 : ∀ a : G, e * a = a ∧ a * e = a),
      have h8 : ∀ a : G, e = classical.some (h3 a), from sorry,
      have h9 : ∀ a : G, e = classical.some (h4 a), from sorry,
      show e = (1 : G), from sorry,
    },
    sorry,
  }
end

/--`theorem`
Bipartite Graph is two colorable
Let $G$ be a graph. Then $G$ is 2-colorable if and only if $G$ is bipartite.
`proof`
Let $G$ be a 2-colorable graph, which means we can color every vertex either red or blue, and no edge will have both endpoints colored the same color. Let $A$ denote the subset of vertices colored red, and let $B$ denote the subset of vertices colored blue. Since all vertices of $A$ are red, there are no edges within $A$, and similarly for $B$. This implies that every edge has one endpoint in $A$ and the other in $B$, which means $G$ is bipartite.

Conversely, suppose $G$ is bipartite, that is, we can partition the vertices into two subsets $V_{1}, V_{2}$ every edge has one endpoint in $V_{1}$ and the other in $V_{2}$. Then coloring every vertex of $V_{1}$ red and every vertex of $V_{2}$ blue yields a valid coloring, so $G$ is 2-colorable.

QED

-/
theorem  bipartite_iff_two_colorable {V : Type*} (G : simple_graph V) [fintype V] : (G.colorable 2) ↔ (∃ (A B : Type*) (h : (A ⊕ B) = V), G ≤ cast (congr_arg _ h) (complete_bipartite_graph A B)) :=
FEW SHOT PROMPTS TO CODEX(END)-/


text:
mutual
  @[simp] def isEven : Nat → Bool
    | 0 => true
    | n+1 => isOdd n
  @[simp] def isOdd : Nat → Bool
    | 0 => false
    | n+1 => isEven n
end
termination_by' measure fun
  | Sum.inl n => n
  | Sum.inr n => n
decreasing_by apply Nat.lt_succ_self

theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
  induction x with
  | zero => simp
  | succ x ih => simp [Nat.mul_succ, Nat.add_succ, ih]

def f (x : Nat) : Nat :=
  match x with
  | 0 => 1
  | x + 1 => f x * 2
termination_by' measure id
decreasing_by apply Nat.lt_succ_self

attribute [simp] f

theorem f_succ (x : Nat) : f (x+1) = f x * 2 := by
  simp

theorem f_succ₂ (x : Nat) : f (x+1) = f x * 2 := by
  simp [-f]
  simp

attribute [-simp] f

theorem f_succ₃ (x : Nat) : f (x+1) = f x * 2 := by
  simp
  simp [f]

author: Kha