awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
ext fun _ => rfl

Premises used: sSupHom.ext, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
inst_1 : SupSet β
f : sSupHom α β
⊢ comp (sSupHom.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: sSupHom.ext, 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₁ g₂ : sSupHom β γ
f : sSupHom α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (fun a ↦ comp a f)⟩

Premises used: Iff.mpr, Function.Surjective.forall, sSupHom.ext, DFunLike.ext_iff, congr_arg, Iff.intro, Iff.mp, sSupHom.comp
-- 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₁ f₂ : sSupHom α β
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: sSupHom.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 α
x : CompleteLattice β
s : Set α
inl : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ((fun (x_1 : α) ↦ ⊥) '' ∅))
inr : ∀ (hs : s.Nonempty), Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, 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 α
x : CompleteLattice β
inl : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ∅)
inl₁ inl₂ : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) ⊥
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ((fun (x_1 : α) ↦ ⊥) '' ∅))

Tactic:
rw [Set.image_empty, sSup_empty]

Premises used: 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 : SupSet α
x : CompleteLattice β
s : Set α
hs : s.Nonempty
inr : Eq (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup {⊥})
inr₁ inr₂ : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) ⊥
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))

Tactic:
rw [hs.image_const, sSup_singleton]

Premises used: sSup_singleton, Set.Nonempty.image_const
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
x : CompleteLattice β
⊢ Eq (α := (a : α) → β) (⇑⊥ : (a : α) → β) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : SupSet α
x : CompleteLattice β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((⊥ : (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 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
f g : FrameHom α β
h : Eq (α := (a : α) → β) ((fun (f : FrameHom α β) ↦ f.toFun) f) ((fun (f : FrameHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b)
    (map_top' : { toFun := toFun, map_inf' := map_inf' : InfHom α β }.toFun ⊤ = ⊤)
    (map_sSup' :
      ∀ (s : Set α),
        { toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun (sSup s) =
          sSup ({ toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun '' s))
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : FrameHom α β) ↦ f.toFun)
          { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' })
        ((fun (f : FrameHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' : FrameHom α β } = g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := 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 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
g : FrameHom α β
toFun : α → β
map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b
map_top' : { toFun := toFun, map_inf' := map_inf' : InfHom α β }.toFun ⊤ = ⊤
map_sSup' :
  ∀ (s : Set α),
    { toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun (sSup s) =
      sSup ({ toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun '' s)
h :
  Eq (α := (a : α) → β)
    ((fun (f : FrameHom α β) ↦ f.toFun)
      { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' })
    ((fun (f : FrameHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_inf'_1 : ∀ (a b : α), toFun_1 (a ⊓ b) = toFun_1 a ⊓ toFun_1 b)
    (map_top'_1 : { toFun := toFun_1, map_inf' := map_inf'_1 : InfHom α β }.toFun ⊤ = ⊤)
    (map_sSup'_1 :
      ∀ (s : Set α),
        { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1 : InfTopHom α β }.toFun (sSup s) =
          sSup ({ toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1 : InfTopHom α β }.toFun '' s))
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : FrameHom α β) ↦ f.toFun)
          { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' })
        ((fun (f : FrameHom α β) ↦ f.toFun)
          { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1, map_sSup' := map_sSup'_1 })),
    { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' : FrameHom α β } =
      { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1, map_sSup' := map_sSup'_1 }
⊢ { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' : FrameHom α β } = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := 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 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
toFun : α → β
map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b
map_top' : { toFun := toFun, map_inf' := map_inf' : InfHom α β }.toFun ⊤ = ⊤
map_sSup' :
  ∀ (s : Set α),
    { toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun (sSup s) =
      sSup ({ toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun '' s)
toFun_1 : α → β
map_inf'_1 : ∀ (a b : α), toFun_1 (a ⊓ b) = toFun_1 a ⊓ toFun_1 b
map_top'_1 : { toFun := toFun_1, map_inf' := map_inf'_1 : InfHom α β }.toFun ⊤ = ⊤
map_sSup'_1 :
  ∀ (s : Set α),
    { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1 : InfTopHom α β }.toFun (sSup s) =
      sSup ({ toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1 : InfTopHom α β }.toFun '' s)
h :
  Eq (α := (a : α) → β)
    ((fun (f : FrameHom α β) ↦ f.toFun)
      { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' })
    ((fun (f : FrameHom α β) ↦ f.toFun)
      { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1, map_sSup' := map_sSup'_1 })
⊢ { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' : FrameHom α β } =
    { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1, map_sSup' := map_sSup'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : FrameHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toInfTopHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : FrameHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toLatticeHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: FrameHom.comp, InfTopHom.comp, InfHom.comp, rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : FrameHom α β
⊢ f.comp (FrameHom.id α) = f

Tactic:
ext fun _ => rfl

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

Tactic:
ext fun _ => rfl

Premises used: FrameHom.ext, 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₁ g₂ : FrameHom β γ
f : FrameHom α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (fun a ↦ comp a f)⟩

Premises used: Iff.mpr, FrameHom.ext, Function.Surjective.forall, DFunLike.ext_iff, FrameHom.comp, congr_arg, Iff.intro, Iff.mp
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
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: FrameHom.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 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
f g : CompleteLatticeHom α β
h :
  Eq (α := (a : α) → β) ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) f)
    ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s))
    (map_sSup' :
      ∀ (s : Set α),
        { toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun (sSup s) =
          sSup ({ toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun '' s))
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : CompleteLatticeHom α β) ↦ f.toFun)
          { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' })
        ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' : CompleteLatticeHom α β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := 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 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
g : CompleteLatticeHom α β
toFun : α → β
map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s)
map_sSup' :
  ∀ (s : Set α),
    { toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun (sSup s) =
      sSup ({ toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun '' s)
h :
  Eq (α := (a : α) → β)
    ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' })
    ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_sInf'_1 : ∀ (s : Set α), toFun_1 (sInf s) = sInf (toFun_1 '' s))
    (map_sSup'_1 :
      ∀ (s : Set α),
        { toFun := toFun_1, map_sInf' := map_sInf'_1 : sInfHom α β }.toFun (sSup s) =
          sSup ({ toFun := toFun_1, map_sInf' := map_sInf'_1 : sInfHom α β }.toFun '' s))
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : CompleteLatticeHom α β) ↦ f.toFun)
          { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' })
        ((fun (f : CompleteLatticeHom α β) ↦ f.toFun)
          { toFun := toFun_1, map_sInf' := map_sInf'_1, map_sSup' := map_sSup'_1 })),
    { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' : CompleteLatticeHom α β } =
      { toFun := toFun_1, map_sInf' := map_sInf'_1, map_sSup' := map_sSup'_1 }
⊢ { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' : CompleteLatticeHom α β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := 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 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
toFun : α → β
map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s)
map_sSup' :
  ∀ (s : Set α),
    { toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun (sSup s) =
      sSup ({ toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun '' s)
toFun_1 : α → β
map_sInf'_1 : ∀ (s : Set α), toFun_1 (sInf s) = sInf (toFun_1 '' s)
map_sSup'_1 :
  ∀ (s : Set α),
    { toFun := toFun_1, map_sInf' := map_sInf'_1 : sInfHom α β }.toFun (sSup s) =
      sSup ({ toFun := toFun_1, map_sInf' := map_sInf'_1 : sInfHom α β }.toFun '' s)
h :
  Eq (α := (a : α) → β)
    ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' })
    ((fun (f : CompleteLatticeHom α β) ↦ f.toFun)
      { toFun := toFun_1, map_sInf' := map_sInf'_1, map_sSup' := map_sSup'_1 })
⊢ { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' : CompleteLatticeHom α β } =
    { toFun := toFun_1, map_sInf' := map_sInf'_1, map_sSup' := map_sSup'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
⊢ Eq (α := (a : α) → β) (⇑f.tosInfHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.CompleteLattice
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toBoundedLatticeHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
ext fun _ => rfl

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

Tactic:
ext fun _ => rfl

Premises used: CompleteLatticeHom.ext, 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₁ g₂ : CompleteLatticeHom β γ
f : CompleteLatticeHom α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (fun a ↦ comp a f)⟩

Premises used: Iff.mpr, Function.Surjective.forall, DFunLike.ext_iff, congr_arg, Iff.intro, Iff.mp, CompleteLatticeHom.comp, CompleteLatticeHom.ext
-- 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₁ f₂ : CompleteLatticeHom α β
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: CompleteLatticeHom.comp_apply