awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedLatticeHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Eq (α := (a : α) → α) (⇑(BoundedLatticeHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
a : α
⊢ (BoundedLatticeHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedLatticeHom β γ
g : BoundedLatticeHom α β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedLatticeHom β γ
g : BoundedLatticeHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedLatticeHom β γ
g : BoundedLatticeHom α β
⊢ {
      toSupHom :=
        SupHom.comp.{u_2, u_3, u_4} (β := β) { toFun := (⇑f : (a : β) → γ), map_sup' := ⋯ }
          { toFun := (⇑g : (a : α) → β), map_sup' := ⋯ },
      map_inf' := ⋯ } =
    { toFun := (⇑f : (a : β) → γ), map_sup' := ⋯, map_inf' := ⋯ : LatticeHom β γ }.comp
      { toFun := (⇑g : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ : LatticeHom α β }

Tactic:
rfl

Premises used: LatticeHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedLatticeHom β γ
g : BoundedLatticeHom α β
⊢ { toFun := (⇑(f.comp g) : (a : α) → γ), map_sup' := ⋯, map_inf' := ⋯ } =
    { toFun := (⇑f : (a : β) → γ), map_sup' := ⋯, map_inf' := ⋯ : LatticeHom β γ }.comp
      { toFun := (⇑g : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ : LatticeHom α β }

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedLatticeHom β γ
g : BoundedLatticeHom α β
⊢ Eq (α := SupHom α γ)
    { toFun := Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β), map_sup' := ⋯ }
    (SupHom.comp.{u_2, u_3, u_4} (β := β) { toFun := (⇑f : (a : β) → γ), map_sup' := ⋯ }
      { toFun := (⇑g : (a : α) → β), map_sup' := ⋯ })

Tactic:
rfl

Premises used: SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedLatticeHom β γ
g : BoundedLatticeHom α β
⊢ Eq (α := SupHom α γ) { toFun := (⇑(f.comp g) : (a : α) → γ), map_sup' := ⋯ }
    (SupHom.comp.{u_2, u_3, u_4} (β := β) { toFun := (⇑f : (a : β) → γ), map_sup' := ⋯ }
      { toFun := (⇑g : (a : α) → β), map_sup' := ⋯ })

Tactic:
rfl

Premises used: SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : Lattice δ
inst_4 : BoundedOrder α
inst_5 : BoundedOrder β
inst_6 : BoundedOrder γ
inst_7 : BoundedOrder δ
f : BoundedLatticeHom γ δ
g : BoundedLatticeHom β γ
h : BoundedLatticeHom α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, BoundedLatticeHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedLatticeHom α β
⊢ f.comp (BoundedLatticeHom.id α) = f

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, BoundedLatticeHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedLatticeHom α β
⊢ comp (BoundedLatticeHom.id β) f = f

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, BoundedLatticeHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g₁ g₂ : BoundedLatticeHom β γ
f : BoundedLatticeHom α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => BoundedLatticeHom.ext <| hf.forall.2 <| DFunLike.ext_iff.1 h,
    fun h => congr_arg₂ _ h rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, BoundedLatticeHom.ext, DFunLike.ext_iff, Iff.intro, Iff.mp, BoundedLatticeHom.comp, rfl, congr_arg₂
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: BoundedLatticeHom.comp_apply
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this_1 : Lattice { x : β // P x } := Subtype.lattice (P := P) Psup Pinf
this : BoundedOrder (Subtype P) := Subtype.boundedOrder (p := P) Pbot Ptop
⊢ (LatticeHom.subtypeVal (P := P) Psup Pinf).toFun ⊤ = ⊤

Tactic:
simp [Subtype.coe_top Ptop]

Premises used: Subtype.coe_top
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this_1 : Lattice { x : β // P x } := Subtype.lattice (P := P) Psup Pinf
this : BoundedOrder (Subtype P) := Subtype.boundedOrder (p := P) Pbot Ptop
⊢ (LatticeHom.subtypeVal (P := P) Psup Pinf).toFun ⊥ = ⊥

Tactic:
simp [Subtype.coe_bot Pbot]

Premises used: Subtype.coe_bot
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
β : Type u_3
inst : Lattice β
inst_1 : BoundedOrder β
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
x : { x : β // P x }
⊢ (subtypeVal (P := P) Pbot Ptop Psup Pinf : (a : { x : β // P x }) → β) x = (↑x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
β : Type u_3
inst : Lattice β
inst_1 : BoundedOrder β
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
⊢ Eq (α := (a : { x : β // P x }) → β) (⇑(subtypeVal (P := P) Pbot Ptop Psup Pinf) : (a : { x : β // P x }) → β)
    (Subtype.val (p := fun (x : β) ↦ P x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Max α
inst_1 : Bot α
⊢ Eq (α := InfTopHom αᵒᵈ αᵒᵈ) ((dual : (a : SupBotHom α α) → InfTopHom αᵒᵈ αᵒᵈ) (SupBotHom.id α) : InfTopHom αᵒᵈ αᵒᵈ)
    (InfTopHom.id αᵒᵈ : InfTopHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: InfHom.id, OrderDual, InfTopHom.id, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
g : SupBotHom β γ
f : SupBotHom α β
⊢ Eq (α := InfTopHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((dual : (a : SupBotHom α γ) → InfTopHom αᵒᵈ γᵒᵈ) (g.comp f) : InfTopHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (InfTopHom.comp.{u_2, u_3, u_4} (β := βᵒᵈ) ((dual : (a : SupBotHom β γ) → InfTopHom βᵒᵈ γᵒᵈ) g)
        ((dual : (a : SupBotHom α β) → InfTopHom αᵒᵈ βᵒᵈ) f) :
      InfTopHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: InfTopHom.comp, InfHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Max α
inst_1 : Bot α
⊢ Eq.{u_2 + 1} (α := SupBotHom α α)
    ((Equiv.symm dual : (a : InfTopHom αᵒᵈ αᵒᵈ) → SupBotHom α α) (InfTopHom.id αᵒᵈ) : SupBotHom α α)
    (SupBotHom.id α : SupBotHom α α)

Tactic:
rfl

Premises used: SupHom.id, OrderDual, SupBotHom.id, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
g : InfTopHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : InfTopHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := SupBotHom α γ) ((Equiv.symm dual : (a : InfTopHom αᵒᵈ γᵒᵈ) → SupBotHom α γ) (g.comp f) : SupBotHom α γ)
    (comp.{u_2, u_3, u_4} (β := β) ((Equiv.symm dual : (a : InfTopHom βᵒᵈ γᵒᵈ) → SupBotHom β γ) g)
        ((Equiv.symm dual : (a : InfTopHom αᵒᵈ βᵒᵈ) → SupBotHom α β) f) :
      SupBotHom α γ)

Tactic:
rfl

Premises used: SupBotHom.comp, SupHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Eq (α := BoundedLatticeHom αᵒᵈ αᵒᵈ)
    ((BoundedLatticeHom.dual : (a : BoundedLatticeHom α α) → BoundedLatticeHom αᵒᵈ αᵒᵈ) (BoundedLatticeHom.id α) :
      BoundedLatticeHom αᵒᵈ αᵒᵈ)
    (BoundedLatticeHom.id αᵒᵈ : BoundedLatticeHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: BoundedLatticeHom.id, LatticeHom.id, OrderDual, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Lattice β
inst_3 : BoundedOrder β
inst_4 : Lattice γ
inst_5 : BoundedOrder γ
g : BoundedLatticeHom β γ
f : BoundedLatticeHom α β
⊢ Eq (α := BoundedLatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((BoundedLatticeHom.dual : (a : BoundedLatticeHom α γ) → BoundedLatticeHom αᵒᵈ γᵒᵈ) (g.comp f) :
      BoundedLatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (comp.{u_2, u_3, u_4} (β := βᵒᵈ)
        ((BoundedLatticeHom.dual : (a : BoundedLatticeHom β γ) → BoundedLatticeHom βᵒᵈ γᵒᵈ) g)
        ((BoundedLatticeHom.dual : (a : BoundedLatticeHom α β) → BoundedLatticeHom αᵒᵈ βᵒᵈ) f) :
      BoundedLatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, BoundedLatticeHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Eq.{u_2 + 1} (α := BoundedLatticeHom α α)
    ((Equiv.symm BoundedLatticeHom.dual : (a : BoundedLatticeHom αᵒᵈ αᵒᵈ) → BoundedLatticeHom α α)
        (BoundedLatticeHom.id αᵒᵈ) :
      BoundedLatticeHom α α)
    (BoundedLatticeHom.id α : BoundedLatticeHom α α)

Tactic:
rfl

Premises used: BoundedLatticeHom.id, LatticeHom.id, OrderDual, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Lattice β
inst_3 : BoundedOrder β
inst_4 : Lattice γ
inst_5 : BoundedOrder γ
g : BoundedLatticeHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : BoundedLatticeHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := BoundedLatticeHom α γ)
    ((Equiv.symm BoundedLatticeHom.dual : (a : BoundedLatticeHom αᵒᵈ γᵒᵈ) → BoundedLatticeHom α γ) (g.comp f) :
      BoundedLatticeHom α γ)
    (comp.{u_2, u_3, u_4} (β := β)
        ((Equiv.symm BoundedLatticeHom.dual : (a : BoundedLatticeHom βᵒᵈ γᵒᵈ) → BoundedLatticeHom β γ) g)
        ((Equiv.symm BoundedLatticeHom.dual : (a : BoundedLatticeHom αᵒᵈ βᵒᵈ) → BoundedLatticeHom α β) f) :
      BoundedLatticeHom α γ)

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, BoundedLatticeHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : sSupHomClass F α β
f : F
g : ι → α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⨆ (i : ι), g i) : β) (⨆ (i : ι), (f : (a : α) → β) (g i) : β)

Tactic:
simp [iSup, ← Set.range_comp, Function.comp_def]

Premises used: Set.range_comp, iSup, Function.comp_def
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⨆ (i : ι), ⨆ (j : κ i), g i j) : β)
    (⨆ (i : ι), ⨆ (j : κ i), (f : (a : α) → β) (g i j) : β)

Tactic:
simp_rw [map_iSup]

Premises used: map_iSup
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass F α β
f : F
a b : α
rw :
  Eq.{u_3 + 1} (α := β) (sSup (image (α := α) (⇑f : (a : α) → β) {a, b}) : β)
    ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊔ b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)

Tactic:
rw [← sSup_pair, map_sSup]

Premises used: sSupHomClass.map_sSup, sSup_pair
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass F α β
f : F
a b : α
⊢ Eq.{u_3 + 1} (α := β) (sSup (image (α := α) (⇑f : (a : α) → β) {a, b}) : β)
    ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)

Tactic:
simp only [Set.image_pair, sSup_insert, sSup_singleton]

Premises used: Set.image_pair, sSup_insert, sSup_singleton
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sSup ∅) : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (sSup (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) ∅)) ⊥
rw₂ : Eq.{u_3 + 1} (α := β) (sSup ∅) ⊥
rw₃ rw₄ : Eq.{u_3 + 1} (α := β) ⊥ ⊥
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty]

Premises used: sSupHomClass.map_sSup, sSup_empty, Set.image_empty
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : FrameHomClass F α β
⊢ sSupHomClass F α β

Tactic:
{ ‹FrameHomClass F α β› with }

Premises used: FrameHomClass.map_sSup, sSupHomClass.mk
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : FrameHomClass F α β
⊢ BoundedLatticeHomClass F α β

Tactic:
{ ‹FrameHomClass F α β›, sSupHomClass.toSupBotHomClass with }

Premises used: SupBotHomClass.map_bot, InfTopHomClass.map_top, sSupHomClass.toSupBotHomClass, BoundedLatticeHomClass.mk
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLatticeHomClass F α β
⊢ FrameHomClass F α β

Tactic:
{ ‹CompleteLatticeHomClass F α β›, sInfHomClass.toInfTopHomClass with }

Premises used: sSupHomClass.map_sSup, sInfHomClass.toInfTopHomClass, FrameHomClass.mk
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLatticeHomClass F α β
⊢ BoundedLatticeHomClass F α β

Tactic:
{ sSupHomClass.toSupBotHomClass, sInfHomClass.toInfTopHomClass with }

Premises used: SupBotHomClass.map_bot, InfTopHomClass.map_top, sInfHomClass.toInfTopHomClass, sSupHomClass.toSupBotHomClass, BoundedLatticeHomClass.mk
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : EquivLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : OrderIsoClass F α β
f : F
s : Set α
c : β
⊢ (f : (a : α) → β) (sSup s) ≤ c ↔ sSup ((⇑f : (a : α) → β) '' s) ≤ c

Tactic:
simp only [← le_map_inv_iff, sSup_le_iff, Set.forall_mem_image]

Premises used: le_map_inv_iff, sSup_le_iff, Set.forall_mem_image
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : EquivLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : OrderIsoClass F α β
⊢ CompleteLatticeHomClass F α β

Tactic:
{ OrderIsoClass.tosSupHomClass, OrderIsoClass.tosInfHomClass with }

Premises used: CompleteLatticeHomClass.mk, OrderIsoClass.tosSupHomClass, OrderIsoClass.tosInfHomClass
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
f g : sSupHom α β
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → β) (map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s))
    (h : { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β }.toFun = g.toFun),
    { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
g : sSupHom α β
toFun : α → β
map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s)
h : { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → β) (map_sSup'_1 : ∀ (s : Set α), toFun_1 (sSup s) = sSup (toFun_1 '' s))
    (h :
      { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β }.toFun =
        { toFun := toFun_1, map_sSup' := map_sSup'_1 : sSupHom α β }.toFun),
    { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β } = { toFun := toFun_1, map_sSup' := map_sSup'_1 }
⊢ { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β } = g

Tactic:
cases g
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
toFun : α → β
map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s)
toFun_1 : α → β
map_sSup'_1 : ∀ (s : Set α), toFun_1 (sSup s) = sSup (toFun_1 '' s)
h :
  { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β }.toFun =
    { toFun := toFun_1, map_sSup' := map_sSup'_1 : sSupHom α β }.toFun
⊢ { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β } = { toFun := toFun_1, map_sSup' := map_sSup'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
inst_1 : SupSet β
f : sSupHom α β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
inst_1 : SupSet β
f : α → β
hf : ∀ (s : Set α), f (sSup s) = sSup (f '' s)
⊢ (⇑{ toFun := f, map_sSup' := hf : sSupHom α β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
inst_1 : SupSet β
f g : sSupHom α β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
inst_1 : SupSet β
f : sSupHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
inst_1 : SupSet β
f : sSupHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
s : Set α
rw : sSup s = sSup (id '' s)
rw₁ rw₂ : sSup s = sSup s
⊢ id (sSup s) = sSup (id '' s)

Tactic:
rw [id, Set.image_id]

Premises used: id, Set.image_id
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : SupSet α
⊢ Eq (α := (a : α) → α) (⇑(sSupHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : SupSet α
a : α
⊢ (sSupHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
rw :
  Eq.{u_4 + 1} (α := γ) (sSup ((fun (x : α) ↦ (f : (a : β) → γ) ((g : (a : α) → β) x : β)) '' s))
    (sSup (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) '' s))
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) (sSup s))
    (sSup (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) '' s))

Tactic:
rw [comp_apply, map_sSup, map_sSup, Set.image_image]

Premises used: Set.image_image, sSupHomClass.map_sSup, Function.comp_apply
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ Eq.{u_4 + 1} (α := γ) (sSup ((fun (x : α) ↦ (f : (a : β) → γ) ((g : (a : α) → β) x : β)) '' s))
    (sSup (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) '' s))

Tactic:
simp only [Function.comp]

Premises used: Function.comp
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SupSet α
inst_1 : SupSet β
inst_2 : SupSet γ
f : sSupHom β γ
g : sSupHom α β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl