[GOAL]
α β : DistLatCat
e : ↑α ≃o ↑β
⊢ { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) } ≫
      {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : DistLatCat
e : ↑α ≃o ↑β
x✝ : (forget DistLatCat).obj α
⊢ ↑({ toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) } ≫
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : DistLatCat
e : ↑α ≃o ↑β
⊢ {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) } ≫
      { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : DistLatCat
e : ↑α ≃o ↑β
x✝ : (forget DistLatCat).obj β
⊢ ↑({
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) } ≫
          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ ↑f a = ⊤ ↔ a = ⊤
[PROOFSTEP]
letI : TopHomClass F α β := OrderIsoClass.toTopHomClass
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : TopHomClass F α β := OrderIsoClass.toTopHomClass
⊢ ↑f a = ⊤ ↔ a = ⊤
[PROOFSTEP]
rw [← map_top f, (EquivLike.injective f).eq_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ ↑f a = ⊥ ↔ a = ⊥
[PROOFSTEP]
letI : BotHomClass F α β := OrderIsoClass.toBotHomClass
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : BotHomClass F α β := OrderIsoClass.toBotHomClass
⊢ ↑f a = ⊥ ↔ a = ⊥
[PROOFSTEP]
rw [← map_bot f, (EquivLike.injective f).eq_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
g : TopHom α β
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝, map_top' := map_top'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_top' := map_top'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
toFun✝¹ : α → β
map_top'✝¹ : toFun✝¹ ⊤ = ⊤
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝¹, map_top' := map_top'✝¹ }.toFun = { toFun := toFun✝, map_top' := map_top'✝ }.toFun
⊢ { toFun := toFun✝¹, map_top' := map_top'✝¹ } = { toFun := toFun✝, map_top' := map_top'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f : TopHom β γ
g : TopHom α β
⊢ (↑f ∘ ↑g) ⊤ = ⊤
[PROOFSTEP]
rw [comp_apply, map_top, map_top]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← TopHom.comp_apply, h, TopHom.comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (↑f ⊓ ↑g) ⊤ = ⊤
[PROOFSTEP]
rw [Pi.inf_apply, map_top, map_top, inf_top_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (↑f ⊔ ↑g) ⊤ = ⊤
[PROOFSTEP]
rw [Pi.sup_apply, map_top, map_top, sup_top_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
f g : BotHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
g : BotHom α β
toFun✝ : α → β
map_bot'✝ : toFun✝ ⊥ = ⊥
h : { toFun := toFun✝, map_bot' := map_bot'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_bot' := map_bot'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
toFun✝¹ : α → β
map_bot'✝¹ : toFun✝¹ ⊥ = ⊥
toFun✝ : α → β
map_bot'✝ : toFun✝ ⊥ = ⊥
h : { toFun := toFun✝¹, map_bot' := map_bot'✝¹ }.toFun = { toFun := toFun✝, map_bot' := map_bot'✝ }.toFun
⊢ { toFun := toFun✝¹, map_bot' := map_bot'✝¹ } = { toFun := toFun✝, map_bot' := map_bot'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
f : BotHom β γ
g : BotHom α β
⊢ (↑f ∘ ↑g) ⊥ = ⊥
[PROOFSTEP]
rw [comp_apply, map_bot, map_bot]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
g : BotHom β γ
f₁ f₂ : BotHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← BotHom.comp_apply, h, BotHom.comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Bot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
f✝ g✝ f g : BotHom α β
⊢ (↑f ⊓ ↑g) ⊥ = ⊥
[PROOFSTEP]
rw [Pi.inf_apply, map_bot, map_bot, inf_bot_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Bot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f✝ g✝ f g : BotHom α β
⊢ (↑f ⊔ ↑g) ⊥ = ⊥
[PROOFSTEP]
rw [Pi.sup_apply, map_bot, map_bot, sup_bot_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedOrderHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊤ = ⊤
map_bot'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f => f.toFun) g
⊢ { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_top'✝¹ : OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } ⊤ = ⊤
map_bot'✝¹ : OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } ⊥ = ⊥
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊤ = ⊤
map_bot'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]


[GOAL]
α β : LatCat
e : ↑α ≃o ↑β
⊢ { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) } ≫
      {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : LatCat
e : ↑α ≃o ↑β
x✝ : (forget LatCat).obj α
⊢ ↑({ toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) } ≫
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : LatCat
e : ↑α ≃o ↑β
⊢ {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) } ≫
      { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : LatCat
e : ↑α ≃o ↑β
x✝ : (forget LatCat).obj β
⊢ ↑({
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) } ≫
          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
α β : FinPartOrd
e : ↑α.toPartOrdCat ≃o ↑β.toPartOrdCat
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : FinPartOrd
e : ↑α.toPartOrdCat ≃o ↑β.toPartOrdCat
x✝ : (forget FinPartOrd).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x✝ = ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : FinPartOrd
e : ↑α.toPartOrdCat ≃o ↑β.toPartOrdCat
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : FinPartOrd
e : ↑α.toPartOrdCat ≃o ↑β.toPartOrdCat
x✝ : (forget FinPartOrd).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x✝ = ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
⊢ ConcreteCategory HeytAlgCat
[PROOFSTEP]
dsimp [HeytAlgCat]
[GOAL]
⊢ ConcreteCategory (Bundled HeytingAlgebra)
[PROOFSTEP]
infer_instance
  -- Porting note: No idea why it does not find this instance...
[GOAL]
α β : HeytAlgCat
e : ↑α ≃o ↑β
⊢ {
        toLatticeHom :=
          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
        map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) } ≫
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
        map_himp' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : HeytAlgCat
e : ↑α ≃o ↑β
x✝ : (forget HeytAlgCat).obj α
⊢ ↑({
            toLatticeHom :=
              { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) } ≫
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                map_inf' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
            map_himp' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : HeytAlgCat
e : ↑α ≃o ↑β
⊢ {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
        map_himp' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) } ≫
      {
        toLatticeHom :=
          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
        map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : HeytAlgCat
e : ↑α ≃o ↑β
x✝ : (forget HeytAlgCat).obj β
⊢ ↑({
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                map_inf' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
            map_himp' :=
              (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) } ≫
          {
            toLatticeHom :=
              { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
⊢ ConcreteCategory FrmCat
[PROOFSTEP]
unfold FrmCat
[GOAL]
⊢ ConcreteCategory (Bundled Frame)
[PROOFSTEP]
infer_instance
[GOAL]
α β : FrmCat
e : ↑α ≃o ↑β
⊢ {
        toInfTopHom :=
          { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
      {
        toInfTopHom :=
          {
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : FrmCat
e : ↑α ≃o ↑β
x✝ : (forget FrmCat).obj α
⊢ ↑({
            toInfTopHom :=
              { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
                map_top' := (_ : ↑e ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
          {
            toInfTopHom :=
              {
                toInfHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_inf' :=
                      (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
                map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : FrmCat
e : ↑α ≃o ↑β
⊢ {
        toInfTopHom :=
          {
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
      {
        toInfTopHom :=
          { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : FrmCat
e : ↑α ≃o ↑β
x✝ : (forget FrmCat).obj β
⊢ ↑({
            toInfTopHom :=
              {
                toInfHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_inf' :=
                      (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
                map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
          {
            toInfTopHom :=
              { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
                map_top' := (_ : ↑e ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
src✝ : SupHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
inst✝ : InfHomClass F α β
src✝ : InfHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
rw [← inf_eq_left, ← map_inf, inf_eq_left.2 h]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
a b : α
c : (fun x => β) (a ⊔ b)
⊢ ↑f (a ⊔ b) ≤ c ↔ ↑f a ⊔ ↑f b ≤ c
[PROOFSTEP]
simp only [← le_map_inv_iff, sup_le_iff]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
a b : α
c : (fun x => β) (a ⊓ b)
⊢ c ≤ ↑f (a ⊓ b) ↔ c ≤ ↑f a ⊓ ↑f b
[PROOFSTEP]
simp only [← map_inv_le_iff, le_inf_iff]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : Lattice β
inst✝¹ : BoundedOrder β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
h : Disjoint a b
⊢ Disjoint (↑f a) (↑f b)
[PROOFSTEP]
rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : Lattice β
inst✝¹ : BoundedOrder β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
h : Codisjoint a b
⊢ Codisjoint (↑f a) (↑f b)
[PROOFSTEP]
rw [codisjoint_iff, ← map_sup, h.eq_top, map_top]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ ↑f (a \ b) = ↑f a \ ↑f b
[PROOFSTEP]
rw [sdiff_eq, sdiff_eq, map_inf, map_compl']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ ↑f (a ∆ b) = ↑f a ∆ ↑f b
[PROOFSTEP]
rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
f g : SupHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
g : SupHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sup' := map_sup'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun = { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } = { toFun := toFun✝, map_sup' := map_sup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ (↑f ∘ ↑g) (a ⊔ b) = (↑f ∘ ↑g) a ⊔ (↑f ∘ ↑g) b
[PROOFSTEP]
rw [comp_apply, map_sup, map_sup]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ ↑f (↑g a) ⊔ ↑f (↑g b) = (↑f ∘ ↑g) a ⊔ (↑f ∘ ↑g) b
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← SupHom.comp_apply, h, SupHom.comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ (↑f ⊔ ↑g) (a ⊔ b) = (↑f ⊔ ↑g) a ⊔ (↑f ⊔ ↑g) b
[PROOFSTEP]
rw [Pi.sup_apply, map_sup, map_sup]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ ↑f a ⊔ ↑f b ⊔ (↑g a ⊔ ↑g b) = (↑f ⊔ ↑g) a ⊔ (↑f ⊔ ↑g) b
[PROOFSTEP]
exact sup_sup_sup_comm _ _ _ _
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
f g : InfHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
g : InfHom α β
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
h : { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_inf' := map_inf'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
toFun✝¹ : α → β
map_inf'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊓ b) = toFun✝¹ a ⊓ toFun✝¹ b
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
h : { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }.toFun = { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun
⊢ { toFun := toFun✝¹, map_inf' := map_inf'✝¹ } = { toFun := toFun✝, map_inf' := map_inf'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
f : InfHom β γ
g : InfHom α β
a b : α
⊢ (↑f ∘ ↑g) (a ⊓ b) = (↑f ∘ ↑g) a ⊓ (↑f ∘ ↑g) b
[PROOFSTEP]
rw [comp_apply, map_inf, map_inf]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
f : InfHom β γ
g : InfHom α β
a b : α
⊢ ↑f (↑g a) ⊓ ↑f (↑g b) = (↑f ∘ ↑g) a ⊓ (↑f ∘ ↑g) b
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
g : InfHom β γ
f₁ f₂ : InfHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← InfHom.comp_apply, h, InfHom.comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f g : InfHom α β
a b : α
⊢ (↑f ⊓ ↑g) (a ⊓ b) = (↑f ⊓ ↑g) a ⊓ (↑f ⊓ ↑g) b
[PROOFSTEP]
rw [Pi.inf_apply, map_inf, map_inf]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f g : InfHom α β
a b : α
⊢ ↑f a ⊓ ↑f b ⊓ (↑g a ⊓ ↑g b) = (↑f ⊓ ↑g) a ⊓ (↑f ⊓ ↑g) b
[PROOFSTEP]
exact inf_inf_inf_comm _ _ _ _
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
f g : SupBotHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
g : SupBotHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_bot'✝ : SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_bot' := map_bot'✝ } =
    (fun f => f.toFun) g
⊢ { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_bot' := map_bot'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_bot'✝¹ : SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_bot'✝ : SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_bot' := map_bot'✝¹ } =
    (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_bot' := map_bot'✝ }
⊢ { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_bot' := map_bot'✝¹ } =
    { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_bot' := map_bot'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
f g : InfTopHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
g : InfTopHom α β
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
h :
  (fun f => f.toFun) { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ } =
    (fun f => f.toFun) g
⊢ { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
toFun✝¹ : α → β
map_inf'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊓ b) = toFun✝¹ a ⊓ toFun✝¹ b
map_top'✝¹ : InfHom.toFun { toFun := toFun✝¹, map_inf' := map_inf'✝¹ } ⊤ = ⊤
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
h :
  (fun f => f.toFun) { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ } =
    (fun f => f.toFun) { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }
⊢ { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ } =
    { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
g : InfTopHom β γ
f₁ f₂ : InfTopHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
f g : LatticeHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
g : LatticeHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ } =
    (fun f => f.toFun) g
⊢ { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } a ⊓
        SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ } =
    (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }
⊢ { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ } =
    { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]
[GOAL]
case inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : b ≤ a
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
[GOAL]
case inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : b ≤ a
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedLatticeHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedLatticeHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_top'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊤ = ⊤
map_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } a ⊓
        SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } b
map_top'✝¹ :
  SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom ⊤ = ⊤
map_bot'✝¹ :
  SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_top'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊤ = ⊤
map_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_top' := map_top'✝, map_bot' := map_bot'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
⊢ (fun f => ↑f) (withTopWithBot (LatticeHom.id α)) = (fun f => ↑f) (BoundedLatticeHom.id (WithTop (WithBot α)))
[PROOFSTEP]
refine' (congr_arg Option.map _).trans Option.map_id
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
⊢ (fun x => ↑(LatticeHom.withBot (LatticeHom.id α)).toSupHom x) = id
[PROOFSTEP]
rw [withBot_id]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
⊢ (fun x => ↑(LatticeHom.id (WithBot α)).toSupHom x) = id
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ withTopWithBot (comp f g) = BoundedLatticeHom.comp (withTopWithBot f) (withTopWithBot g)
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ ↑(withTopWithBot (comp f g)) a✝ = ↑(BoundedLatticeHom.comp (withTopWithBot f) (withTopWithBot g)) a✝
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
⊢ b ≠ ⊥
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ False
[PROOFSTEP]
refine' P.not_bot_mem (_)
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts
[PROOFSTEP]
rw [h] at hb
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts
[PROOFSTEP]
exact hb
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥
[PROOFSTEP]
simp_rw [← P.supParts]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ sup P.parts id = ⊥
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ eq_empty_iff_forall_not_mem.2 fun b hb ↦ P.not_bot_mem _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ sup P.parts id = ⊥
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ sup ∅ id = ⊥
[PROOFSTEP]
exact Finset.sup_empty
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : sup P.parts id = ⊥
b : α
hb : b ∈ P.parts
⊢ ⊥ ∈ P.parts
[PROOFSTEP]
rwa [← le_bot_iff.1 ((le_sup hb).trans h.le)]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ Finset.Nonempty P.parts ↔ a ≠ ⊥
[PROOFSTEP]
rw [nonempty_iff_ne_empty, not_iff_not, parts_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : Inhabited (Finpartition ⊥) := inferInstance
P : Finpartition ⊥
⊢ P = default
[PROOFSTEP]
ext a
[GOAL]
case parts.a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a✝ : α
P✝ : Finpartition a✝
src✝ : Inhabited (Finpartition ⊥) := inferInstance
P : Finpartition ⊥
a : α
⊢ a ∈ P.parts ↔ a ∈ default.parts
[PROOFSTEP]
exact iff_of_false (fun h ↦ P.ne_bot h <| le_bot_iff.1 <| P.le h) (not_mem_empty a)
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
⊢ P = default
[PROOFSTEP]
have h : ∀ b ∈ P.parts, b = a := fun _ hb ↦ (ha.le_iff.mp <| P.le hb).resolve_left (P.ne_bot hb)
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ (b : α), b ∈ P.parts → b = a
⊢ P = default
[PROOFSTEP]
ext b
[GOAL]
case parts.a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ (b : α), b ∈ P.parts → b = a
b : α
⊢ b ∈ P.parts ↔ b ∈ default.parts
[PROOFSTEP]
refine' Iff.trans ⟨h b, _⟩ mem_singleton.symm
[GOAL]
case parts.a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ (b : α), b ∈ P.parts → b = a
b : α
⊢ b = a → b ∈ P.parts
[PROOFSTEP]
rintro rfl
[GOAL]
case parts.a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
b : α
P✝ : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ (b_1 : α), b_1 ∈ P.parts → b_1 = b
⊢ b ∈ P.parts
[PROOFSTEP]
obtain ⟨c, hc⟩ := P.parts_nonempty ha.1
[GOAL]
case parts.a.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
b : α
P✝ : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ (b_1 : α), b_1 ∈ P.parts → b_1 = b
c : α
hc : c ∈ P.parts
⊢ b ∈ P.parts
[PROOFSTEP]
simp_rw [← h c hc]
[GOAL]
case parts.a.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
b : α
P✝ : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ (b_1 : α), b_1 ∈ P.parts → b_1 = b
c : α
hc : c ∈ P.parts
⊢ c ∈ P.parts
[PROOFSTEP]
exact hc
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q R : Finpartition a
hPQ : P ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ P.parts
⊢ ∃ c, c ∈ R.parts ∧ b ≤ c
[PROOFSTEP]
obtain ⟨c, hc, hbc⟩ := hPQ hb
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q R : Finpartition a
hPQ : P ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c, c ∈ R.parts ∧ b ≤ c
[PROOFSTEP]
obtain ⟨d, hd, hcd⟩ := hQR hc
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q R : Finpartition a
hPQ : P ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hcd : c ≤ d
⊢ ∃ c, c ∈ R.parts ∧ b ≤ c
[PROOFSTEP]
exact ⟨d, hd, hbc.trans hcd⟩
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
⊢ P = Q
[PROOFSTEP]
ext b
[GOAL]
case parts.a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
⊢ b ∈ P.parts ↔ b ∈ Q.parts
[PROOFSTEP]
refine' ⟨fun hb ↦ _, fun hb ↦ _⟩
[GOAL]
case parts.a.refine'_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
⊢ b ∈ Q.parts
[PROOFSTEP]
obtain ⟨c, hc, hbc⟩ := hPQ hb
[GOAL]
case parts.a.refine'_1.intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ b ∈ Q.parts
[PROOFSTEP]
obtain ⟨d, hd, hcd⟩ := hQP hc
[GOAL]
case parts.a.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ b ∈ Q.parts
[PROOFSTEP]
rwa [hbc.antisymm]
[GOAL]
case parts.a.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ b
[PROOFSTEP]
rwa [P.disjoint.eq_of_le hb hd (P.ne_bot hb) (hbc.trans hcd)]
[GOAL]
case parts.a.refine'_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
⊢ b ∈ P.parts
[PROOFSTEP]
obtain ⟨c, hc, hbc⟩ := hQP hb
[GOAL]
case parts.a.refine'_2.intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
⊢ b ∈ P.parts
[PROOFSTEP]
obtain ⟨d, hd, hcd⟩ := hPQ hc
[GOAL]
case parts.a.refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ∈ P.parts
[PROOFSTEP]
rwa [hbc.antisymm]
[GOAL]
case parts.a.refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
src✝ : LE (Finpartition a) := inferInstance
P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ b
[PROOFSTEP]
rwa [Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)]
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
⊢ P ≤ ⊤
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
⊢ P ≤ ⊤
[PROOFSTEP]
intro x hx
[GOAL]
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
x : α
hx : x ∈ P.parts
⊢ ∃ c, c ∈ ⊤.parts ∧ x ≤ c
[PROOFSTEP]
simpa [h, P.ne_bot hx] using P.le hx
[GOAL]
case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : ¬a = ⊥
⊢ P ≤ ⊤
[PROOFSTEP]
exact fun b hb ↦ ⟨a, mem_singleton_self _, P.le hb⟩
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
⊢ ⊤.parts ⊆ {a}
[PROOFSTEP]
intro b hb
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb : b ∈ ⊤.parts
⊢ b ∈ {a}
[PROOFSTEP]
have hb : b ∈ Finpartition.parts (dite _ _ _) := hb
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
hb : b ∈ (if ha : a = ⊥ then copy (Finpartition.empty α) (_ : ⊥ = a) else indiscrete ha).parts
⊢ b ∈ {a}
[PROOFSTEP]
split_ifs at hb
[GOAL]
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : a = ⊥
hb : b ∈ (copy (Finpartition.empty α) (_ : ⊥ = a)).parts
⊢ b ∈ {a}
[PROOFSTEP]
simp only [copy_parts, empty_parts, not_mem_empty] at hb
[GOAL]
case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : ¬a = ⊥
hb : b ∈ (indiscrete h✝).parts
⊢ b ∈ {a}
[PROOFSTEP]
exact hb
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ SupIndep (image (fun bc => bc.fst ⊓ bc.snd) (P.parts ×ˢ Q.parts)) id
[PROOFSTEP]
rw [supIndep_iff_disjoint_erase]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ ∀ (i : α),
    i ∈ image (fun bc => bc.fst ⊓ bc.snd) (P.parts ×ˢ Q.parts) →
      Disjoint (id i) (sup (erase (image (fun bc => bc.fst ⊓ bc.snd) (P.parts ×ˢ Q.parts)) i) id)
[PROOFSTEP]
simp only [mem_image, and_imp, exists_prop, forall_exists_index, id.def, Prod.exists, mem_product,
  Finset.disjoint_sup_right, mem_erase, Ne.def]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ ∀ (i x x_1 : α),
    x ∈ P.parts →
      x_1 ∈ Q.parts →
        x ⊓ x_1 = i →
          ∀ ⦃i_1 : α⦄, ¬i_1 = i → ∀ (x x_2 : α), x ∈ P.parts → x_2 ∈ Q.parts → x ⊓ x_2 = i_1 → Disjoint i i_1
[PROOFSTEP]
rintro _ x₁ y₁ hx₁ hy₁ rfl _ h x₂ y₂ hx₂ hy₂ rfl
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
x₂ y₂ : α
hx₂ : x₂ ∈ P.parts
hy₂ : y₂ ∈ Q.parts
h : ¬x₂ ⊓ y₂ = x₁ ⊓ y₁
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)
[PROOFSTEP]
rcases eq_or_ne x₁ x₂ with (rfl | xdiff)
[GOAL]
case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
⊢ Disjoint (x₁ ⊓ y₁) (x₁ ⊓ y₂)
[PROOFSTEP]
refine' Disjoint.mono inf_le_right inf_le_right (Q.disjoint hy₁ hy₂ _)
[GOAL]
case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
⊢ y₁ ≠ y₂
[PROOFSTEP]
intro t
[GOAL]
case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
t : y₁ = y₂
⊢ False
[PROOFSTEP]
simp [t] at h
[GOAL]
case inr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
x₂ y₂ : α
hx₂ : x₂ ∈ P.parts
hy₂ : y₂ ∈ Q.parts
h : ¬x₂ ⊓ y₂ = x₁ ⊓ y₁
xdiff : x₁ ≠ x₂
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)
[PROOFSTEP]
exact Disjoint.mono inf_le_left inf_le_left (P.disjoint hx₁ hx₂ xdiff)
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ sup (image (fun bc => bc.fst ⊓ bc.snd) (P.parts ×ˢ Q.parts)) id = a
[PROOFSTEP]
rw [sup_image, comp.left_id, sup_product_left]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (sup P.parts fun i => sup Q.parts fun i' => (i, i').fst ⊓ (i, i').snd) = a
[PROOFSTEP]
trans P.parts.sup id ⊓ Q.parts.sup id
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (sup P.parts fun i => sup Q.parts fun i' => (i, i').fst ⊓ (i, i').snd) = sup P.parts id ⊓ sup Q.parts id
[PROOFSTEP]
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (sup P.parts fun i => sup Q.parts fun i' => i ⊓ i') = sup P.parts fun i => sup Q.parts fun i_1 => id i ⊓ id i_1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ sup P.parts id ⊓ sup Q.parts id = a
[PROOFSTEP]
rw [P.supParts, Q.supParts, inf_idem]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c, c ∈ P.parts ∧ b ≤ c
[PROOFSTEP]
obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)
[GOAL]
case intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q : Finpartition a
c : α × α
hc : c ∈ P.parts ×ˢ Q.parts
hb : c.fst ⊓ c.snd ∈ (P ⊓ Q).parts
⊢ ∃ c_1, c_1 ∈ P.parts ∧ c.fst ⊓ c.snd ≤ c_1
[PROOFSTEP]
rw [mem_product] at hc
[GOAL]
case intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q : Finpartition a
c : α × α
hc : c.fst ∈ P.parts ∧ c.snd ∈ Q.parts
hb : c.fst ⊓ c.snd ∈ (P ⊓ Q).parts
⊢ ∃ c_1, c_1 ∈ P.parts ∧ c.fst ⊓ c.snd ≤ c_1
[PROOFSTEP]
exact ⟨c.1, hc.1, inf_le_left⟩
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c, c ∈ Q.parts ∧ b ≤ c
[PROOFSTEP]
obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)
[GOAL]
case intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q : Finpartition a
c : α × α
hc : c ∈ P.parts ×ˢ Q.parts
hb : c.fst ⊓ c.snd ∈ (P ⊓ Q).parts
⊢ ∃ c_1, c_1 ∈ Q.parts ∧ c.fst ⊓ c.snd ≤ c_1
[PROOFSTEP]
rw [mem_product] at hc
[GOAL]
case intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q : Finpartition a
c : α × α
hc : c.fst ∈ P.parts ∧ c.snd ∈ Q.parts
hb : c.fst ⊓ c.snd ∈ (P ⊓ Q).parts
⊢ ∃ c_1, c_1 ∈ Q.parts ∧ c.fst ⊓ c.snd ≤ c_1
[PROOFSTEP]
exact ⟨c.2, hc.2, inf_le_right⟩
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
⊢ ∃ c, c ∈ (Q ⊓ R).parts ∧ b ≤ c
[PROOFSTEP]
obtain ⟨c, hc, hbc⟩ := hPQ hb
[GOAL]
case intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c, c ∈ (Q ⊓ R).parts ∧ b ≤ c
[PROOFSTEP]
obtain ⟨d, hd, hbd⟩ := hPR hb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hbd : b ≤ d
⊢ ∃ c, c ∈ (Q ⊓ R).parts ∧ b ≤ c
[PROOFSTEP]
have h := _root_.le_inf hbc hbd
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
src✝¹ : PartialOrder (Finpartition a) := inferInstance
src✝ : Inf (Finpartition a) := inferInstance
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hbd : b ≤ d
h : b ≤ c ⊓ d
⊢ ∃ c, c ∈ (Q ⊓ R).parts ∧ b ≤ c
[PROOFSTEP]
refine'
  ⟨c ⊓ d,
    mem_erase_of_ne_of_mem (ne_bot_of_le_ne_bot (P.ne_bot hb) h) (mem_image.2 ⟨(c, d), mem_product.2 ⟨hc, hd⟩, rfl⟩), h⟩
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c, c ∈ P.parts ∧ c ≤ b
[PROOFSTEP]
by_contra H
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ False
[PROOFSTEP]
refine' Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) _)
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ Disjoint b a
[PROOFSTEP]
rw [← P.supParts, Finset.disjoint_sup_right]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ ∀ ⦃i : α⦄, i ∈ P.parts → Disjoint b (id i)
[PROOFSTEP]
rintro c hc
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
⊢ Disjoint b (id c)
[PROOFSTEP]
obtain ⟨d, hd, hcd⟩ := h hc
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ Disjoint b (id c)
[PROOFSTEP]
refine' (Q.disjoint hb hd _).mono_right hcd
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ≠ d
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
⊢ False
[PROOFSTEP]
simp only [not_exists, not_and] at H
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
H : ∀ (x : α), x ∈ P.parts → ¬x ≤ b
⊢ False
[PROOFSTEP]
exact H _ hc hcd
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ card Q.parts ≤ card P.parts
[PROOFSTEP]
classical
have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
choose f hP hf using this
rw [← card_attach]
refine' card_le_card_of_inj_on (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ _
exact
  Subtype.coe_injective
    (Q.disjoint.elim b.2 c.2 fun H ↦
      P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ card Q.parts ≤ card P.parts
[PROOFSTEP]
have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
this : ∀ (b : α), b ∈ Q.parts → ∃ c, c ∈ P.parts ∧ c ≤ b
⊢ card Q.parts ≤ card P.parts
[PROOFSTEP]
choose f hP hf using this
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ card Q.parts ≤ card P.parts
[PROOFSTEP]
rw [← card_attach]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ card (attach Q.parts) ≤ card P.parts
[PROOFSTEP]
refine' card_le_card_of_inj_on (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ _
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h✝ : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
b : { x // x ∈ Q.parts }
x✝¹ : b ∈ attach Q.parts
c : { x // x ∈ Q.parts }
x✝ : c ∈ attach Q.parts
h : (fun b => f ↑b (_ : ↑b ∈ Q.parts)) b = (fun b => f ↑b (_ : ↑b ∈ Q.parts)) c
⊢ b = c
[PROOFSTEP]
exact
  Subtype.coe_injective
    (Q.disjoint.elim b.2 c.2 fun H ↦
      P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ SupIndep (Finset.biUnion (attach P.parts) fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) id
[PROOFSTEP]
rw [supIndep_iff_pairwiseDisjoint]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ Set.PairwiseDisjoint (↑(Finset.biUnion (attach P.parts) fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts)) id
[PROOFSTEP]
rintro a ha b hb h
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a✝ b✝ c : α
P✝ : Finpartition a✝
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a✝
Q : (i : α) → i ∈ P.parts → Finpartition i
a : α
ha : a ∈ ↑(Finset.biUnion (attach P.parts) fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts)
b : α
hb : b ∈ ↑(Finset.biUnion (attach P.parts) fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts)
h : a ≠ b
⊢ (Disjoint on id) a b
[PROOFSTEP]
rw [Finset.mem_coe, Finset.mem_biUnion] at ha hb
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a✝ b✝ c : α
P✝ : Finpartition a✝
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a✝
Q : (i : α) → i ∈ P.parts → Finpartition i
a : α
ha : ∃ a_1, a_1 ∈ attach P.parts ∧ a ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts
b : α
hb : ∃ a, a ∈ attach P.parts ∧ b ∈ (Q ↑a (_ : ↑a ∈ P.parts)).parts
h : a ≠ b
⊢ (Disjoint on id) a b
[PROOFSTEP]
obtain ⟨⟨A, hA⟩, -, ha⟩ := ha
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a✝ b✝ c : α
P✝ : Finpartition a✝
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a✝
Q : (i : α) → i ∈ P.parts → Finpartition i
a b : α
hb : ∃ a, a ∈ attach P.parts ∧ b ∈ (Q ↑a (_ : ↑a ∈ P.parts)).parts
h : a ≠ b
A : α
hA : A ∈ P.parts
ha : a ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
⊢ (Disjoint on id) a b
[PROOFSTEP]
obtain ⟨⟨B, hB⟩, -, hb⟩ := hb
[GOAL]
case intro.mk.intro.intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a✝ b✝ c : α
P✝ : Finpartition a✝
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a✝
Q : (i : α) → i ∈ P.parts → Finpartition i
a b : α
h : a ≠ b
A : α
hA : A ∈ P.parts
ha : a ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
B : α
hB : B ∈ P.parts
hb : b ∈ (Q ↑{ val := B, property := hB } (_ : ↑{ val := B, property := hB } ∈ P.parts)).parts
⊢ (Disjoint on id) a b
[PROOFSTEP]
obtain rfl | hAB := eq_or_ne A B
[GOAL]
case intro.mk.intro.intro.mk.intro.inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a✝ b✝ c : α
P✝ : Finpartition a✝
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a✝
Q : (i : α) → i ∈ P.parts → Finpartition i
a b : α
h : a ≠ b
A : α
hA : A ∈ P.parts
ha : a ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
hB : A ∈ P.parts
hb : b ∈ (Q ↑{ val := A, property := hB } (_ : ↑{ val := A, property := hB } ∈ P.parts)).parts
⊢ (Disjoint on id) a b
[PROOFSTEP]
exact (Q A hA).disjoint ha hb h
[GOAL]
case intro.mk.intro.intro.mk.intro.inr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a✝ b✝ c : α
P✝ : Finpartition a✝
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a✝
Q : (i : α) → i ∈ P.parts → Finpartition i
a b : α
h : a ≠ b
A : α
hA : A ∈ P.parts
ha : a ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
B : α
hB : B ∈ P.parts
hb : b ∈ (Q ↑{ val := B, property := hB } (_ : ↑{ val := B, property := hB } ∈ P.parts)).parts
hAB : A ≠ B
⊢ (Disjoint on id) a b
[PROOFSTEP]
exact (P.disjoint hA hB hAB).mono ((Q A hA).le ha) ((Q B hB).le hb)
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ sup (Finset.biUnion (attach P.parts) fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) id = a
[PROOFSTEP]
simp_rw [sup_biUnion]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (sup (attach P.parts) fun x => sup (Q ↑x (_ : ↑x ∈ P.parts)).parts id) = a
[PROOFSTEP]
trans (sup P.parts id)
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (sup (attach P.parts) fun x => sup (Q ↑x (_ : ↑x ∈ P.parts)).parts id) = sup P.parts id
[PROOFSTEP]
rw [eq_comm, ← Finset.sup_attach]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (sup (attach P.parts) fun x => id ↑x) = sup (attach P.parts) fun x => sup (Q ↑x (_ : ↑x ∈ P.parts)).parts id
[PROOFSTEP]
exact sup_congr rfl fun b _hb ↦ (Q b.1 b.2).supParts.symm
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ sup P.parts id = a
[PROOFSTEP]
exact P.supParts
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
h : ⊥ ∈ Finset.biUnion (attach P.parts) fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts
⊢ False
[PROOFSTEP]
rw [Finset.mem_biUnion] at h
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
h : ∃ a_1, a_1 ∈ attach P.parts ∧ ⊥ ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts
⊢ False
[PROOFSTEP]
obtain ⟨⟨A, hA⟩, -, h⟩ := h
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : ⊥ ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
⊢ False
[PROOFSTEP]
exact (Q A hA).not_bot_mem h
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ b ∈ (bind P Q).parts ↔ ∃ A hA, b ∈ (Q A hA).parts
[PROOFSTEP]
rw [bind, mem_biUnion]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts) ↔ ∃ A hA, b ∈ (Q A hA).parts
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts) → ∃ A hA, b ∈ (Q A hA).parts
[PROOFSTEP]
rintro ⟨⟨A, hA⟩, -, h⟩
[GOAL]
case mp.intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
⊢ ∃ A hA, b ∈ (Q A hA).parts
[PROOFSTEP]
exact ⟨A, hA, h⟩
[GOAL]
case mpr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A hA, b ∈ (Q A hA).parts) → ∃ a_2, a_2 ∈ attach P.parts ∧ b ∈ (Q ↑a_2 (_ : ↑a_2 ∈ P.parts)).parts
[PROOFSTEP]
rintro ⟨A, hA, h⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts
[PROOFSTEP]
exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ card (bind P Q).parts = ∑ A in attach P.parts, card (Q ↑A (_ : ↑A ∈ P.parts)).parts
[PROOFSTEP]
apply card_biUnion
[GOAL]
case h
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ ∀ (x : { x // x ∈ P.parts }),
    x ∈ attach P.parts →
      ∀ (y : { x // x ∈ P.parts }),
        y ∈ attach P.parts →
          x ≠ y → Disjoint ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) x) ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) y)
[PROOFSTEP]
rintro ⟨b, hb⟩ - ⟨c, hc⟩ - hbc
[GOAL]
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
⊢ Disjoint ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb })
    ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc })
[PROOFSTEP]
rw [Finset.disjoint_left]
[GOAL]
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
⊢ ∀ ⦃a_1 : α⦄,
    a_1 ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb } →
      ¬a_1 ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
[PROOFSTEP]
rintro d hdb hdc
[GOAL]
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
d : α
hdb : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb }
hdc : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
⊢ False
[PROOFSTEP]
rw [Ne.def, Subtype.mk_eq_mk] at hbc
[GOAL]
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ¬b = c
d : α
hdb : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb }
hdc : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
⊢ False
[PROOFSTEP]
exact
  (Q b hb).ne_bot hdb
    (eq_bot_iff.2 <| (le_inf ((Q b hb).le hdb) <| (Q c hc).le hdc).trans <| (P.disjoint hb hc hbc).le_bot)
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ SupIndep (insert b P.parts) id
[PROOFSTEP]
rw [supIndep_iff_pairwiseDisjoint, coe_insert]
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Set.PairwiseDisjoint (insert b ↑P.parts) id
[PROOFSTEP]
exact P.disjoint.insert fun d hd _ ↦ hab.symm.mono_right <| P.le hd
[GOAL]
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ sup (insert b P.parts) id = c
[PROOFSTEP]
rwa [sup_insert, P.supParts, id, _root_.sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b✝ c : α
P : Finpartition a
b : α
⊢ sup (image (fun x => x \ b) P.parts) id = a \ b
[PROOFSTEP]
rw [sup_image, comp.left_id, Finset.sup_sdiff_right, ← id_def, P.supParts]
[GOAL]
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ c ∈ (avoid P b).parts ↔ ∃ d, d ∈ P.parts ∧ ¬d ≤ b ∧ d \ b = c
[PROOFSTEP]
simp only [avoid, ofErase, mem_erase, Ne.def, mem_image, exists_prop, ← exists_and_left, @and_left_comm (c ≠ ⊥)]
[GOAL]
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ (∃ x, x ∈ P.parts ∧ ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d, d ∈ P.parts ∧ ¬d ≤ b ∧ d \ b = c
[PROOFSTEP]
refine' exists_congr fun d ↦ and_congr_right' <| and_congr_left _
[GOAL]
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
d : α
⊢ d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b
[PROOFSTEP]
rw [sdiff_eq_bot_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃ t, t ∈ P.parts ∧ a ∈ t
[PROOFSTEP]
simp_rw [← P.supParts] at ha
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ha : a ∈ sup P.parts id
⊢ ∃ t, t ∈ P.parts ∧ a ∈ t
[PROOFSTEP]
exact mem_sup.1 ha
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = card s
[PROOFSTEP]
convert congr_arg Finset.card P.biUnion_parts
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = card (Finset.biUnion P.parts id)
[PROOFSTEP]
rw [card_biUnion P.supIndep.pairwiseDisjoint]
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = ∑ u in P.parts, card (id u)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
⊢ Set.PairwiseDisjoint (↑(map { toFun := singleton, inj' := (_ : Injective singleton) } s)) id
[PROOFSTEP]
rw [Finset.coe_map]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
⊢ Set.PairwiseDisjoint (↑{ toFun := singleton, inj' := (_ : Injective singleton) } '' ↑s) id
[PROOFSTEP]
exact Finset.pairwiseDisjoint_range_singleton.subset (Set.image_subset_range _ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
⊢ sup (map { toFun := singleton, inj' := (_ : Injective singleton) } s) id = s
[PROOFSTEP]
rw [sup_map, comp.left_id, Embedding.coeFn_mk, Finset.sup_singleton']
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
⊢ ¬⊥ ∈ map { toFun := singleton, inj' := (_ : Injective singleton) } s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
P✝ : Finpartition s✝
s : Finset α
src✝ : Bot (Finpartition s) := inferInstance
P : Finpartition s
t : Finset α
ht : t ∈ ⊥.parts
⊢ ∃ c, c ∈ P.parts ∧ t ≤ c
[PROOFSTEP]
rw [mem_bot_iff] at ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
P✝ : Finpartition s✝
s : Finset α
src✝ : Bot (Finpartition s) := inferInstance
P : Finpartition s
t : Finset α
ht : ∃ a, a ∈ s ∧ {a} = t
⊢ ∃ c, c ∈ P.parts ∧ t ≤ c
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ := ht
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P✝ : Finpartition s✝
s : Finset α
src✝ : Bot (Finpartition s) := inferInstance
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃ c, c ∈ P.parts ∧ {a} ≤ c
[PROOFSTEP]
obtain ⟨t, ht, hat⟩ := P.exists_mem ha
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
P✝ : Finpartition s✝
s : Finset α
src✝ : Bot (Finpartition s) := inferInstance
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
hat : a ∈ t
⊢ ∃ c, c ∈ P.parts ∧ {a} ≤ c
[PROOFSTEP]
exact ⟨t, ht, singleton_subset_iff.2 hat⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P✝ P : Finpartition s
⊢ card P.parts ≤ card s
[PROOFSTEP]
rw [← card_bot s]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P✝ P : Finpartition s
⊢ card P.parts ≤ card ⊥.parts
[PROOFSTEP]
exact card_mono bot_le
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : x ∈ ↑(image (fun Q => filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s) (powerset F))
y : Finset α
hy : y ∈ ↑(image (fun Q => filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s) (powerset F))
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
⊢ x = y
[PROOFSTEP]
rw [mem_coe, mem_image] at hx hy
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : ∃ a, a ∈ powerset F ∧ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ a ↔ i ∈ t)) s = x
y : Finset α
hy : ∃ a, a ∈ powerset F ∧ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ a ↔ i ∈ t)) s = y
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
⊢ x = y
[PROOFSTEP]
obtain ⟨Q, hQ, rfl⟩ := hx
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
y : Finset α
hy : ∃ a, a ∈ powerset F ∧ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ a ↔ i ∈ t)) s = y
z : α
hz2 : z ∈ id y
Q : Finset (Finset α)
hQ : Q ∈ powerset F
h : filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠ y
hz1 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s)
⊢ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s = y
[PROOFSTEP]
obtain ⟨R, hR, rfl⟩ := hy
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ powerset F
hz1 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s)
R : Finset (Finset α)
hR : R ∈ powerset F
hz2 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
⊢ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s =
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
[PROOFSTEP]
suffices h' : Q = R
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ powerset F
hz1 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s)
R : Finset (Finset α)
hR : R ∈ powerset F
hz2 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
h' : Q = R
⊢ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s =
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
[PROOFSTEP]
subst h'
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ powerset F
hz1 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s)
hR : Q ∈ powerset F
hz2 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s
⊢ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s =
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s
[PROOFSTEP]
exact of_eq_true (eq_self (filter (fun i ↦ ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s))
[GOAL]
case h'
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ powerset F
hz1 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s)
R : Finset (Finset α)
hR : R ∈ powerset F
hz2 : z ∈ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
⊢ Q = R
[PROOFSTEP]
rw [id, mem_filter] at hz1 hz2
[GOAL]
case h'
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ powerset F
hz1 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ z ∈ t)
R : Finset (Finset α)
hR : R ∈ powerset F
hz2 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ z ∈ t)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
⊢ Q = R
[PROOFSTEP]
rw [mem_powerset] at hQ hR
[GOAL]
case h'
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ z ∈ t)
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ z ∈ t)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
⊢ Q = R
[PROOFSTEP]
ext i
[GOAL]
case h'.a
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ z ∈ t)
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ z ∈ t)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
i : Finset α
⊢ i ∈ Q ↔ i ∈ R
[PROOFSTEP]
refine' ⟨fun hi ↦ _, fun hi ↦ _⟩
[GOAL]
case h'.a.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ z ∈ t)
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ z ∈ t)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
i : Finset α
hi : i ∈ Q
⊢ i ∈ R
[PROOFSTEP]
rwa [hz2.2 _ (hQ hi), ← hz1.2 _ (hQ hi)]
[GOAL]
case h'.a.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ z ∈ t)
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ z ∈ t)
h :
  filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s ≠
    filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ R ↔ i ∈ t)) s
i : Finset α
hi : i ∈ R
⊢ i ∈ Q
[PROOFSTEP]
rwa [hz1.2 _ (hR hi), ← hz2.2 _ (hR hi)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
⊢ sup (image (fun Q => filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s) (powerset F)) id = s
[PROOFSTEP]
refine' (Finset.sup_le fun t ht ↦ _).antisymm fun a ha ↦ _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : t ∈ image (fun Q => filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s) (powerset F)
⊢ id t ≤ s
[PROOFSTEP]
rw [mem_image] at ht
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : ∃ a, a ∈ powerset F ∧ filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ a ↔ i ∈ t)) s = t
⊢ id t ≤ s
[PROOFSTEP]
obtain ⟨A, _, rfl⟩ := ht
[GOAL]
case refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F A : Finset (Finset α)
left✝ : A ∈ powerset F
⊢ id (filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ A ↔ i ∈ t)) s) ≤ s
[PROOFSTEP]
exact s.filter_subset _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ a ∈ sup (image (fun Q => filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s) (powerset F)) id
[PROOFSTEP]
rw [mem_sup]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ ∃ v, v ∈ image (fun Q => filter (fun i => ∀ (t : Finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s) (powerset F) ∧ a ∈ id v
[PROOFSTEP]
refine'
  ⟨s.filter fun i ↦ ∀ t, t ∈ F → ((t ∈ F.filter fun u ↦ a ∈ u) ↔ i ∈ t),
    mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _), mem_filter.2 ⟨ha, fun t ht ↦ _⟩⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ filter (fun u => a ∈ u) F ↔ a ∈ t
[PROOFSTEP]
rw [mem_filter]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
P : Finpartition s✝
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ F ∧ a ∈ t ↔ a ∈ t
[PROOFSTEP]
exact and_iff_right ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
⊢ t ∈ (atomise s F).parts ↔ Finset.Nonempty t ∧ ∃ Q x, filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s = t
[PROOFSTEP]
simp only [atomise, ofErase, bot_eq_empty, mem_erase, mem_image, nonempty_iff_ne_empty, mem_singleton, and_comm,
  mem_powerset, exists_prop]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
hs : Finset.Nonempty s
⊢ (atomise s ∅).parts = {s}
[PROOFSTEP]
simp only [atomise, powerset_empty, image_singleton, not_mem_empty, IsEmpty.forall_iff, imp_true_iff, filter_True]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
hs : Finset.Nonempty s
⊢ (ofErase {s} (_ : SupIndep {s} id) (_ : sup {s} id = s)).parts = {s}
[PROOFSTEP]
exact erase_eq_of_not_mem (not_mem_singleton.2 hs.ne_empty.symm)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
⊢ Finset.biUnion (filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts) id = t
[PROOFSTEP]
ext a
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ Finset.biUnion (filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts) id ↔ a ∈ t
[PROOFSTEP]
refine' mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ _⟩
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
⊢ ∃ a_1, a_1 ∈ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ∧ a ∈ id a_1
[PROOFSTEP]
obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)
[GOAL]
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ (atomise s F).parts
hau : a ∈ u
⊢ ∃ a_1, a_1 ∈ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ∧ a ∈ id a_1
[PROOFSTEP]
refine' ⟨u, mem_filter.2 ⟨hu, fun b hb ↦ _, _, hau⟩, hau⟩
[GOAL]
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ (atomise s F).parts
hau : a ∈ u
b : α
hb : b ∈ u
⊢ b ∈ t
[PROOFSTEP]
obtain ⟨Q, _hQ, rfl⟩ := (mem_atomise.1 hu).2
[GOAL]
case a.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s ∈ (atomise s F).parts
hau : a ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s
hb : b ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s
⊢ b ∈ t
[PROOFSTEP]
rw [mem_filter] at hau hb
[GOAL]
case a.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ a ∈ u)
hb : b ∈ s ∧ ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ b ∈ u)
⊢ b ∈ t
[PROOFSTEP]
rwa [← hb.2 _ ht, hau.2 _ ht]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
⊢ card (filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts) ≤ 2 ^ (card F - 1)
[PROOFSTEP]
suffices h :
  ((atomise s F).parts.filter fun u ↦ u ⊆ t ∧ u.Nonempty) ⊆
    (F.erase t).powerset.image fun P ↦ s.filter fun i ↦ ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
h :
  filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ (x : Finset α), x ∈ F → (x ∈ insert t P ↔ i ∈ x)) s) (powerset (erase F t))
⊢ card (filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts) ≤ 2 ^ (card F - 1)
[PROOFSTEP]
refine' (card_le_of_subset h).trans (card_image_le.trans _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
h :
  filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ (x : Finset α), x ∈ F → (x ∈ insert t P ↔ i ∈ x)) s) (powerset (erase F t))
⊢ card (powerset (erase F t)) ≤ 2 ^ (card F - 1)
[PROOFSTEP]
rw [card_powerset, card_erase_of_mem ht]
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
⊢ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ (x : Finset α), x ∈ F → (x ∈ insert t P ↔ i ∈ x)) s) (powerset (erase F t))
[PROOFSTEP]
rw [subset_iff]
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts →
      x ∈ image (fun P => filter (fun i => ∀ (x : Finset α), x ∈ F → (x ∈ insert t P ↔ i ∈ x)) s) (powerset (erase F t))
[PROOFSTEP]
simp_rw [mem_image, mem_powerset, mem_filter, and_imp, Finset.Nonempty, exists_imp, mem_atomise, and_imp,
  Finset.Nonempty, exists_imp]
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄ (x_1 : α),
    x_1 ∈ x →
      ∀ (x_2 : Finset (Finset α)),
        x_2 ⊆ F →
          filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ x_2 ↔ i ∈ u)) s = x →
            x ⊆ t →
              ∀ (x_4 : α),
                x_4 ∈ x →
                  ∃ a, a ⊆ erase F t ∧ filter (fun i => ∀ (x : Finset α), x ∈ F → (x ∈ insert t a ↔ i ∈ x)) s = x
[PROOFSTEP]
rintro P' i hi P PQ rfl hy₂ j _hj
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P✝ : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s
hy₂ : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s ⊆ t
j : α
_hj : j ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s
⊢ ∃ a,
    a ⊆ erase F t ∧
      filter (fun i => ∀ (x : Finset α), x ∈ F → (x ∈ insert t a ↔ i ∈ x)) s =
        filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s
[PROOFSTEP]
refine' ⟨P.erase t, erase_subset_erase _ PQ, _⟩
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P✝ : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s
hy₂ : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s ⊆ t
j : α
_hj : j ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s
⊢ filter (fun i => ∀ (x : Finset α), x ∈ F → (x ∈ insert t (erase P t) ↔ i ∈ x)) s =
    filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ P ↔ i ∈ u)) s
[PROOFSTEP]
simp only [insert_erase (((mem_filter.1 hi).2 _ ht).2 <| hy₂ hi)]