awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : SupSet α
⊢ Eq (α := sInfHom αᵒᵈ αᵒᵈ) ((sSupHom.dual : (a : sSupHom α α) → sInfHom αᵒᵈ αᵒᵈ) (sSupHom.id α) : sInfHom αᵒᵈ αᵒᵈ)
    (sInfHom.id αᵒᵈ : sInfHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: sInfHom.id, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SupSet α
inst_1 : SupSet β
inst_2 : SupSet γ
g : sSupHom β γ
f : sSupHom α β
⊢ Eq (α := sInfHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((sSupHom.dual : (a : sSupHom α γ) → sInfHom αᵒᵈ γᵒᵈ) (g.comp f) : sInfHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (sInfHom.comp.{u_2, u_3, u_4} (β := βᵒᵈ) ((sSupHom.dual : (a : sSupHom β γ) → sInfHom βᵒᵈ γᵒᵈ) g)
        ((sSupHom.dual : (a : sSupHom α β) → sInfHom αᵒᵈ βᵒᵈ) f) :
      sInfHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: sInfHom.comp, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : SupSet α
⊢ Eq.{u_2 + 1} (α := sSupHom α α)
    ((Equiv.symm sSupHom.dual : (a : sInfHom αᵒᵈ αᵒᵈ) → sSupHom α α) (sInfHom.id αᵒᵈ) : sSupHom α α)
    (sSupHom.id α : sSupHom α α)

Tactic:
rfl

Premises used: sSupHom.id, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SupSet α
inst_1 : SupSet β
inst_2 : SupSet γ
g : sInfHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : sInfHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := sSupHom α γ) ((Equiv.symm sSupHom.dual : (a : sInfHom αᵒᵈ γᵒᵈ) → sSupHom α γ) (g.comp f) : sSupHom α γ)
    (comp.{u_2, u_3, u_4} (β := β) ((Equiv.symm sSupHom.dual : (a : sInfHom βᵒᵈ γᵒᵈ) → sSupHom β γ) g)
        ((Equiv.symm sSupHom.dual : (a : sInfHom αᵒᵈ βᵒᵈ) → sSupHom α β) f) :
      sSupHom α γ)

Tactic:
rfl

Premises used: sSupHom.comp, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ Eq (α := CompleteLatticeHom αᵒᵈ αᵒᵈ)
    ((CompleteLatticeHom.dual : (a : CompleteLatticeHom α α) → CompleteLatticeHom αᵒᵈ αᵒᵈ) (CompleteLatticeHom.id α) :
      CompleteLatticeHom αᵒᵈ αᵒᵈ)
    (CompleteLatticeHom.id αᵒᵈ : CompleteLatticeHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: CompleteLatticeHom.id, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
g : CompleteLatticeHom β γ
f : CompleteLatticeHom α β
⊢ Eq (α := CompleteLatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((CompleteLatticeHom.dual : (a : CompleteLatticeHom α γ) → CompleteLatticeHom αᵒᵈ γᵒᵈ) (g.comp f) :
      CompleteLatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (comp.{u_2, u_3, u_4} (β := βᵒᵈ)
        ((CompleteLatticeHom.dual : (a : CompleteLatticeHom β γ) → CompleteLatticeHom βᵒᵈ γᵒᵈ) g)
        ((CompleteLatticeHom.dual : (a : CompleteLatticeHom α β) → CompleteLatticeHom αᵒᵈ βᵒᵈ) f) :
      CompleteLatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: sInfHom.comp, CompleteLatticeHom.comp, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ Eq.{u_2 + 1} (α := CompleteLatticeHom α α)
    ((Equiv.symm CompleteLatticeHom.dual : (a : CompleteLatticeHom αᵒᵈ αᵒᵈ) → CompleteLatticeHom α α)
        (CompleteLatticeHom.id αᵒᵈ) :
      CompleteLatticeHom α α)
    (CompleteLatticeHom.id α : CompleteLatticeHom α α)

Tactic:
rfl

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

Tactic:
rfl

Premises used: sInfHom.comp, CompleteLatticeHom.comp, OrderDual, 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 α β
f : α → β
s : Set (Set β)
⊢ ⋂ t ∈ s, f ⁻¹' t = sInf (preimage f '' s)

Tactic:
simp only [Set.sInf_eq_sInter, Set.sInter_image]

Premises used: Set.sInf_eq_sInter, Set.sInter_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 : FunLike F α β
f : α → β
s : Set (Set β)
⊢ ⋃ t ∈ s, f ⁻¹' t = sSup (preimage f '' s)

Tactic:
simp only [Set.sSup_eq_sUnion, Set.sUnion_image]

Premises used: Set.sSup_eq_sUnion, Set.sUnion_image
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
f : α → β
⊢ (⇑(setPreimage f) : (a : Set β) → Set α) = preimage f

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
f : α → β
s : Set β
⊢ (setPreimage f : (a : Set β) → Set α) s = f ⁻¹' s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := CompleteLatticeHom (Set α) (Set α)) (setPreimage id) (CompleteLatticeHom.id (Set α))

Tactic:
rfl

Premises used: Set.Mem, CompleteLatticeHom.id, setOf, CompleteLatticeHom.setPreimage, Set.preimage, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
g : β → γ
f : α → β
⊢ setPreimage (g ∘ f) = (setPreimage f).comp (setPreimage g)

Tactic:
rfl

Premises used: Set.Mem, setOf, CompleteLatticeHom.setPreimage, Set.preimage, sInfHom.comp, CompleteLatticeHom.comp, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
f : α → β
s : Set (Set α)
⊢ f '' sSup s = sSup (image f '' s)

Tactic:
Set.image_sUnion

Premises used: Set.sUnion, Set.image_sUnion
-- 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 α β
e : α ≃ β
s : Set α
⊢ (fun (s : Set β) ↦ ((⇑e.symm : (a : β) → α) '' s : Set α)) ((fun (s : Set α) ↦ ((⇑e : (a : α) → β) '' s : Set β)) s) =
    s

Tactic:
simp only [← image_comp, Equiv.symm_comp_self, id, image_id']

Premises used: Equiv.symm_comp_self, Set.image_id', id, Set.image_comp
-- 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 α β
e : α ≃ β
s : Set β
⊢ (fun (s : Set α) ↦ ((⇑e : (a : α) → β) '' s : Set β)) ((fun (s : Set β) ↦ ((⇑e.symm : (a : β) → α) '' s : Set α)) s) =
    s

Tactic:
simp only [← image_comp, Equiv.self_comp_symm, id, image_id']

Premises used: Set.image_id', id, Equiv.self_comp_symm, Set.image_comp
-- 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 α β
e : α ≃ β
a b : Set α
h :
  LE.le.{u_3} (α := Set β)
    (({ toFun := fun (s : Set α) ↦ (⇑e : (a : α) → β) '' s, invFun := fun (s : Set β) ↦ (⇑e.symm : (a : β) → α) '' s,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Set α) → Set β)
        a :
      Set β)
    (({ toFun := fun (s : Set α) ↦ (⇑e : (a : α) → β) '' s, invFun := fun (s : Set β) ↦ (⇑e.symm : (a : β) → α) '' s,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Set α) → Set β)
        b :
      Set β)
⊢ a ≤ b

Tactic:
simpa using @monotone_image _ _ e.symm _ _ h

Premises used: Set.monotone_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 : FunLike F α β
inst_1 : CompleteLattice α
x : α × α
s : Set (α × α)
simp_rw : sSup (Prod.fst '' s) ⊔ (sSup s).2 = sSup ((fun (x : α × α) ↦ x.1 ⊔ x.2) '' s)
simp_rw₁ : sSup (Prod.fst '' s) ⊔ sSup (Prod.snd '' s) = sSup ((fun (x : α × α) ↦ x.1 ⊔ x.2) '' s)
simp_rw₂ : Eq.{u_2 + 1} (α := α) ((⨆ a ∈ s, a.1) ⊔ ⨆ a ∈ s, a.2) (⨆ a ∈ s, a.1 ⊔ a.2)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun (x : α × α) ↦ x.1 ⊔ x.2) '' s)

Tactic:
simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]

Premises used: iSup_sup_eq, Prod.fst_sSup, sSup_image, Prod.snd_sSup
-- 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 α
x : α × α
s : Set (α × α)
simp_rw : sInf (Prod.fst '' s) ⊓ (sInf s).2 = sInf ((fun (x : α × α) ↦ x.1 ⊓ x.2) '' s)
simp_rw₁ : sInf (Prod.fst '' s) ⊓ sInf (Prod.snd '' s) = sInf ((fun (x : α × α) ↦ x.1 ⊓ x.2) '' s)
simp_rw₂ : Eq.{u_2 + 1} (α := α) ((⨅ a ∈ s, a.1) ⊓ ⨅ a ∈ s, a.2) (⨅ a ∈ s, a.1 ⊓ a.2)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun (x : α × α) ↦ x.1 ⊓ x.2) '' s)

Tactic:
simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]

Premises used: sInf_image, Prod.fst_sInf, iInf_inf_eq, Prod.snd_sInf
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : CompleteLattice α
x : α × α
⊢ (supsSupHom : (a : α × α) → α) x = x.1 ⊔ x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
inst : CompleteLattice α
x : α × α
⊢ (infsInfHom : (a : α × α) → α) x = x.1 ⊓ x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : SemilatticeSup α
inst_2 : SemilatticeSup β
inst_3 : SupHomClass F α β
f : F
a b : α
h : a ≤ b
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊔ b) : β) ((f : (a : α) → β) b : β)
rw₂ rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]

Premises used: Iff.mpr, sup_eq_right, SupHomClass.map_sup
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : SemilatticeSup α
inst_2 : SemilatticeSup β
inst_3 : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ (f : (a : α) → β) (a ⊔ b) ≤ c ↔ (f : (a : α) → β) a ⊔ (f : (a : α) → β) b ≤ c

Tactic:
simp only [← le_map_inv_iff, sup_le_iff]

Premises used: sup_le_iff, le_map_inv_iff
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : SemilatticeInf α
inst_2 : SemilatticeInf β
f : F
inst_3 : InfHomClass F α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
x y : α
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩

Premises used: OrderHomClass.mono, Iff.intro
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : SemilatticeInf α
inst_2 : SemilatticeInf β
f : F
inst_3 : InfHomClass F α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
x y : α
refine : ∀ (h : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)), x ≤ y
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : SemilatticeInf α
inst_2 : SemilatticeInf β
f : F
inst_3 : InfHomClass F α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
x y : α
h : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
rwa : x ⊓ y = x
rwa₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x ⊓ y) : β) ((f : (a : α) → β) x : β)
rwa₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x ⊓ (f : (a : α) → β) y : β) ((f : (a : α) → β) x : β)
rwa₃ rwa₄ rwa₅ rwa₆ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ x ≤ y

Tactic:
rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left]

Premises used: Function.Injective.eq_iff, InfHomClass.map_inf, inf_eq_left
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Max β
inst_3 : Max γ
inst_4 : Max δ
f g : SupHom α β
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → β) (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b)
    (h : { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun = g.toFun),
    { toFun := toFun, map_sup' := map_sup' : SupHom α β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Max β
inst_3 : Max γ
inst_4 : Max δ
g : SupHom α β
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
h : { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → β) (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b)
    (h :
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun =
        { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun),
    { toFun := toFun, map_sup' := map_sup' : SupHom α β } = { toFun := toFun_1, map_sup' := map_sup'_1 }
⊢ { toFun := toFun, map_sup' := map_sup' : SupHom α β } = g

Tactic:
cases g
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Max β
inst_3 : Max γ
inst_4 : Max δ
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
toFun_1 : α → β
map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b
h :
  { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun =
    { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun
⊢ { toFun := toFun, map_sup' := map_sup' : SupHom α β } = { toFun := toFun_1, map_sup' := map_sup'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Max β
f : α → β
hf : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
⊢ (⇑{ toFun := f, map_sup' := hf : SupHom α β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Max β
f g : SupHom α β
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.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Max β
f : SupHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
inst : Max α
a : α
⊢ (SupHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Max β
inst_3 : Max γ
inst_4 : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
rw :
  Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) ⊔ (f : (a : β) → γ) ((g : (a : α) → β) b : β) : γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) a ⊔
        Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) b :
      γ)
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) (a ⊔ b))
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) a ⊔
      Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) b)

Tactic:
rw [comp_apply, map_sup, map_sup]

Premises used: SupHomClass.map_sup, Function.comp_apply
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Max β
inst_3 : Max γ
inst_4 : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) ⊔ (f : (a : β) → γ) ((g : (a : α) → β) b : β) : γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) a ⊔
        Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) b :
      γ)

Tactic:
rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Max β
inst_2 : Max γ
f : SupHom β γ
g : SupHom α β
⊢ 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.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Max β
inst_2 : Max γ
f : SupHom β γ
g : SupHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Max α
inst_1 : Max β
inst_2 : Max γ
inst_3 : Max δ
f : SupHom γ δ
g : SupHom β γ
h : SupHom α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

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

Premises used: Iff.mpr, Function.Surjective.forall, DFunLike.ext_iff, SupHom.comp, Iff.intro, SupHom.ext, Iff.mp, rfl, congr_arg₂
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Max β
inst_2 : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
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 [← SupHom.comp_apply, h, SupHom.comp_apply]

Premises used: SupHom.comp_apply
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
b : β
⊢ (⇑(const α b) : (a : α) → β) = Function.const α b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
b : β
a : α
⊢ (const α b : (a : α) → β) a = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : SemilatticeSup β
f g : SupHom α β
a b : α
rw :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b ⊔ ((g : (a : α) → β) a ⊔ (g : (a : α) → β) b) : β)
    (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) a ⊔ ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) b : β)
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) (a ⊔ b) : β)
    (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) a ⊔ ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) b : β)

Tactic:
rw [Pi.sup_apply, map_sup, map_sup]

Premises used: Pi.sup_apply, SupHomClass.map_sup
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b ⊔ ((g : (a : α) → β) a ⊔ (g : (a : α) → β) b) : β)
    (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) a ⊔ ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) b : β)

Tactic:
sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b ⊔ ((g : (a : α) → β) a ⊔ (g : (a : α) → β) b) : β)
    (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) a ⊔ ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) b : β)

Tactic:
exact sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
f g : SupHom α β
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
inst_2 : Bot β
⊢ Eq (α := (a : α) → β) (⇑⊥ : (a : α) → β) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
inst_2 : Top β
⊢ Eq (α := (a : α) → β) (⇑⊤ : (a : α) → β) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
f g : SupHom α β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f ⊔ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
inst_2 : Bot β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((⊥ : (a : α) → β) a : β) (⊥ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
inst_2 : Top β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((⊤ : (a : α) → β) a : β) (⊤ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : SemilatticeSup β
toFun₁ toFun₂ : α → β
map_sup₁ : ∀ (a b : α), toFun₁ (a ⊔ b) = toFun₁ a ⊔ toFun₁ b
map_sup₂ : ∀ (a b : α), toFun₂ (a ⊔ b) = toFun₂ a ⊔ toFun₂ b
⊢ { toFun := toFun₁, map_sup' := map_sup₁ : SupHom α β } ≤ { toFun := toFun₂, map_sup' := map_sup₂ } ↔ toFun₁ ≤ toFun₂

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : SemilatticeSup β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this : SemilatticeSup { x : β // P x } := Subtype.semilatticeSup (P := P) Psup
⊢ ∀ (a b : { x : β // P x }), (↑(a ⊔ b) : β) = (↑a : β) ⊔ (↑b : β)

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lattice
Goal:
β : Type u_3
inst : SemilatticeSup β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
x : { x : β // P x }
⊢ (subtypeVal (P := P) Psup : (a : { x : β // P x }) → β) x = (↑x : β)

Tactic:
rfl

Premises used: rfl