awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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)
⊢ { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' : CompleteLatticeHom α β } = g
have 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 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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 (α × α)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun (x : α × α) ↦ x.1 ⊔ x.2) '' s)
have simp_rw : sSup (Prod.fst '' s) ⊔ (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]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun (x : α × α) ↦ x.1 ⊔ x.2) '' s)
have simp_rw₁ : sSup (Prod.fst '' s) ⊔ sSup (Prod.snd '' s) = sSup ((fun (x : α × α) ↦ x.1 ⊔ x.2) '' s)
Tactic: simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun (x : α × α) ↦ x.1 ⊔ x.2) '' s)
have simp_rw₂ : Eq.{u_2 + 1} (α := α) ((⨆ a ∈ s, a.1) ⊔ ⨆ a ∈ s, a.2) (⨆ a ∈ s, a.1 ⊔ a.2)
Tactic: simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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 (α × α)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun (x : α × α) ↦ x.1 ⊓ x.2) '' s)
have simp_rw : sInf (Prod.fst '' s) ⊓ (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]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun (x : α × α) ↦ x.1 ⊓ x.2) '' s)
have simp_rw₁ : sInf (Prod.fst '' s) ⊓ sInf (Prod.snd '' s) = sInf ((fun (x : α × α) ↦ x.1 ⊓ x.2) '' s)
Tactic: simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
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)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun (x : α × α) ↦ x.1 ⊓ x.2) '' s)
have simp_rw₂ : Eq.{u_2 + 1} (α := α) ((⨅ a ∈ s, a.1) ⊓ ⨅ a ∈ s, a.2) (⨅ a ∈ s, a.1 ⊓ a.2)
Tactic: simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
Tactic: rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊔ b) : β) ((f : (a : α) → β) b : β)
Tactic: rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
Tactic: rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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
have refine : ∀ (h : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)), x ≤ y
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : β)
⊢ x ≤ y
have rwa : x ⊓ y = x
Tactic: rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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
⊢ x ≤ y
have rwa₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x ⊓ y) : β) ((f : (a : α) → β) x : β)
Tactic: rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : β)
⊢ x ≤ y
have rwa₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x ⊓ (f : (a : α) → β) y : β) ((f : (a : α) → β) x : β)
Tactic: rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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
⊢ { toFun := toFun, map_sup' := map_sup' : SupHom α β } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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} (α := γ)
    (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)
have 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 :
    γ)
Tactic: rw [comp_apply, map_sup, map_sup]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← SupHom.comp_apply, h, SupHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← SupHom.comp_apply, h, SupHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← SupHom.comp_apply, h, SupHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 : α) → β) ⊔ (⇑g : (a : α) → β)) (a ⊔ b) : β)
    (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) a ⊔ ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) b : β)
have 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 : β)
Tactic: rw [Pi.sup_apply, map_sup, map_sup]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 δ
f g : LatticeHom α β
h : Eq (α := (a : α) → β) ((fun (f : LatticeHom α β) ↦ f.toFun) f) ((fun (f : LatticeHom α β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b)
  (map_inf' :
    ∀ (a b : α),
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
          { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' })
      ((fun (f : LatticeHom α β) ↦ f.toFun) g)),
  { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
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 δ
g : LatticeHom α β
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_inf' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b
h :
  Eq (α := (a : α) → β)
    ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' })
    ((fun (f : LatticeHom α β) ↦ f.toFun) g)
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β } = g
have obtain : ∀ (toFun_1 : α → β) (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b)
  (map_inf'_1 :
    ∀ (a b : α),
      { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun (a ⊓ b) =
        { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun a ⊓
          { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun b)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' })
      ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 })),
  { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
have inl : ∀ (h : a ≤ b), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
inl :
  ∀ (h : a ≤ b), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
have inr : ∀ (h : b ≤ a), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
have inl : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
Tactic: rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
inl : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
have inl₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
Tactic: rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
have inr : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
Tactic: rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]