awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
g : CoheytingHom α β
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
map_top' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊤ = ⊤
map_sdiff' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a \ b) =
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a \
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun b
h :
  Eq (α := (a : α) → β)
    ((fun (f : CoheytingHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' })
    ((fun (f : CoheytingHom α β) ↦ f.toFun) g)
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' :
      CoheytingHom α β } =
    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)
  (map_top'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊤ = ⊤)
  (map_sdiff'_1 :
    ∀ (a b : α),
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun (a \ b) =
        { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun a \
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun b)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : CoheytingHom α β) ↦ f.toFun)
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' })
      ((fun (f : CoheytingHom α β) ↦ f.toFun)
        { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
          map_sdiff' := map_sdiff'_1 })),
  { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' :
      CoheytingHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
      map_sdiff' := map_sdiff'_1 }
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
inst_2 : CoheytingAlgebra γ
f₁ f₂ : CoheytingHom α β
g : CoheytingHom β γ
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.Heyting.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
inst_2 : CoheytingAlgebra γ
f₁ f₂ : CoheytingHom α β
g : CoheytingHom β γ
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.Heyting.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
inst_2 : CoheytingAlgebra γ
f₁ f₂ : CoheytingHom α β
g : CoheytingHom β γ
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.Heyting.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : BiheytingAlgebra α
inst_2 : BiheytingAlgebra β
inst_3 : BiheytingAlgebra γ
inst_4 : BiheytingAlgebra δ
f g : BiheytingHom α β
h : Eq (α := (a : α) → β) ((fun (f : BiheytingHom α β) ↦ f.toFun) f) ((fun (f : BiheytingHom α β) ↦ 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)
  (map_himp' :
    ∀ (a b : α),
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a ⇨ b) =
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a ⇨
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun b)
  (map_sdiff' :
    ∀ (a b : α),
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a \ b) =
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a \
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun b)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : BiheytingHom α β) ↦ f.toFun)
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp',
          map_sdiff' := map_sdiff' })
      ((fun (f : BiheytingHom α β) ↦ f.toFun) g)),
  { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' :
      BiheytingHom α β } =
    g
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BiheytingAlgebra α
inst_1 : BiheytingAlgebra β
inst_2 : BiheytingAlgebra γ
f₁ f₂ : BiheytingHom α β
g : BiheytingHom β γ
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.Heyting.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BiheytingAlgebra α
inst_1 : BiheytingAlgebra β
inst_2 : BiheytingAlgebra γ
f₁ f₂ : BiheytingHom α β
g : BiheytingHom β γ
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.Heyting.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BiheytingAlgebra α
inst_1 : BiheytingAlgebra β
inst_2 : BiheytingAlgebra γ
f₁ f₂ : BiheytingHom α β
g : BiheytingHom β γ
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.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
⊢ IsRegular.{u_1} (α := α) ⊥
have rw : Eq.{u_1 + 1} (α := α) ⊥ᶜᶜ ⊥
Tactic: rw [IsRegular, compl_bot, compl_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) ⊥ᶜᶜ ⊥
⊢ IsRegular.{u_1} (α := α) ⊥
have rw₁ : Eq.{u_1 + 1} (α := α) ⊤ᶜ ⊥
Tactic: rw [IsRegular, compl_bot, compl_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) ⊥ᶜᶜ ⊥
rw₁ : Eq.{u_1 + 1} (α := α) ⊤ᶜ ⊥
⊢ IsRegular.{u_1} (α := α) ⊥
have rw₂ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
Tactic: rw [IsRegular, compl_bot, compl_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
⊢ IsRegular.{u_1} (α := α) ⊤
have rw : Eq.{u_1 + 1} (α := α) ⊤ᶜᶜ ⊤
Tactic: rw [IsRegular, compl_top, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) ⊤ᶜᶜ ⊤
⊢ IsRegular.{u_1} (α := α) ⊤
have rw₁ : Eq.{u_1 + 1} (α := α) ⊥ᶜ ⊤
Tactic: rw [IsRegular, compl_top, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) ⊤ᶜᶜ ⊤
rw₁ : Eq.{u_1 + 1} (α := α) ⊥ᶜ ⊤
⊢ IsRegular.{u_1} (α := α) ⊤
have rw₂ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: rw [IsRegular, compl_top, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⊓ b)
have rw : (a ⊓ b)ᶜᶜ = a ⊓ b
Tactic: rw [IsRegular, compl_compl_inf_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
rw : (a ⊓ b)ᶜᶜ = a ⊓ b
⊢ IsRegular (a ⊓ b)
have rw₁ : aᶜᶜ ⊓ bᶜᶜ = a ⊓ b
Tactic: rw [IsRegular, compl_compl_inf_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
rw : (a ⊓ b)ᶜᶜ = a ⊓ b
rw₁ : aᶜᶜ ⊓ bᶜᶜ = a ⊓ b
⊢ IsRegular (a ⊓ b)
have rw₂ : a ⊓ bᶜᶜ = a ⊓ b
Tactic: rw [IsRegular, compl_compl_inf_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
rw : (a ⊓ b)ᶜᶜ = a ⊓ b
rw₁ : aᶜᶜ ⊓ bᶜᶜ = a ⊓ b
rw₂ : a ⊓ bᶜᶜ = a ⊓ b
⊢ IsRegular (a ⊓ b)
have rw₃ : a ⊓ b = a ⊓ b
Tactic: rw [IsRegular, compl_compl_inf_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⇨ b)
have rw : (a ⇨ b)ᶜᶜ = a ⇨ b
Tactic: rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
rw : (a ⇨ b)ᶜᶜ = a ⇨ b
⊢ IsRegular (a ⇨ b)
have rw₁ : aᶜᶜ ⇨ bᶜᶜ = a ⇨ b
Tactic: rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
rw : (a ⇨ b)ᶜᶜ = a ⇨ b
rw₁ : aᶜᶜ ⇨ bᶜᶜ = a ⇨ b
⊢ IsRegular (a ⇨ b)
have rw₂ : a ⇨ bᶜᶜ = a ⇨ b
Tactic: rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
rw : (a ⇨ b)ᶜᶜ = a ⇨ b
rw₁ : aᶜᶜ ⇨ bᶜᶜ = a ⇨ b
rw₂ : a ⇨ bᶜᶜ = a ⇨ b
⊢ IsRegular (a ⇨ b)
have rw₃ : a ⇨ b = a ⇨ b
Tactic: rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
⊢ Disjoint aᶜ b ↔ b ≤ a
have rw : b ≤ aᶜᶜ ↔ b ≤ a
Tactic: rw [← le_compl_iff_disjoint_left, ha.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
rw : b ≤ aᶜᶜ ↔ b ≤ a
⊢ Disjoint aᶜ b ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [← le_compl_iff_disjoint_left, ha.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ Disjoint a bᶜ ↔ a ≤ b
have rw : a ≤ bᶜᶜ ↔ a ≤ b
Tactic: rw [← le_compl_iff_disjoint_right, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
hb : IsRegular b
rw : a ≤ bᶜᶜ ↔ a ≤ b
⊢ Disjoint a bᶜ ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [← le_compl_iff_disjoint_right, hb.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ a ⊔ aᶜ = ⊤
have rw : (a ⊔ aᶜ)ᶜᶜ = ⊤
Tactic: rw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
rw : (a ⊔ aᶜ)ᶜᶜ = ⊤
⊢ a ⊔ aᶜ = ⊤
have rw₁ : (aᶜ ⊓ aᶜᶜ)ᶜ = ⊤
Tactic: rw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
rw : (a ⊔ aᶜ)ᶜᶜ = ⊤
rw₁ : (aᶜ ⊓ aᶜᶜ)ᶜ = ⊤
⊢ a ⊔ aᶜ = ⊤
have rw₂ : Eq.{u_1 + 1} (α := α) ⊥ᶜ ⊤
Tactic: rw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
rw : (a ⊔ aᶜ)ᶜᶜ = ⊤
rw₁ : (aᶜ ⊓ aᶜᶜ)ᶜ = ⊤
rw₂ : Eq.{u_1 + 1} (α := α) ⊥ᶜ ⊤
⊢ a ⊔ aᶜ = ⊤
have rw₃ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: rw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : Regular α
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : α) ≤ (↑(a ⊔ b ⊓ c) : α)
have dsimp : ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ ((↑a : α) ⊔ (↑b : α) ⊓ (↑c : α))ᶜᶜ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : Regular α
⊢ ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ ((↑a : α) ⊔ (↑b : α) ⊓ (↑c : α))ᶜᶜ
have rw : ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ (((↑a : α) ⊔ (↑b : α)) ⊓ ((↑a : α) ⊔ (↑c : α)))ᶜᶜ
Tactic: rw [sup_inf_left, compl_compl_inf_distrib]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : Regular α
rw : ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ (((↑a : α) ⊔ (↑b : α)) ⊓ ((↑a : α) ⊔ (↑c : α)))ᶜᶜ
⊢ ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ ((↑a : α) ⊔ (↑b : α) ⊓ (↑c : α))ᶜᶜ
have rw₁ : ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ
Tactic: rw [sup_inf_left, compl_compl_inf_distrib]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
a : Regular α
⊢ (↑⊤ : α) ≤ (↑(a ⊔ aᶜ) : α)
have dsimp : ⊤ ≤ ((↑a : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
a : Regular α
⊢ ⊤ ≤ ((↑a : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
have rw : ⊤ ≤ ((↑a : α)ᶜ ⊓ (↑a : α)ᶜᶜ)ᶜ
Tactic: rw [compl_sup, inf_compl_eq_bot, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
a : Regular α
rw : ⊤ ≤ ((↑a : α)ᶜ ⊓ (↑a : α)ᶜᶜ)ᶜ
⊢ ⊤ ≤ ((↑a : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
have rw₁ : LE.le.{u_1} (α := α) ⊤ ⊥ᶜ
Tactic: rw [compl_sup, inf_compl_eq_bot, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
a : Regular α
rw : ⊤ ≤ ((↑a : α)ᶜ ⊓ (↑a : α)ᶜᶜ)ᶜ
rw₁ : LE.le.{u_1} (α := α) ⊤ ⊥ᶜ
⊢ ⊤ ≤ ((↑a : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
have rw₂ : LE.le.{u_1} (α := α) ⊤ ⊤
Tactic: rw [compl_sup, inf_compl_eq_bot, compl_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
⊢ (↑(a ⇨ b) : α) = (↑(b ⊔ aᶜ) : α)
have dsimp : (↑a : α) ⇨ (↑b : α) = ((↑b : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
⊢ (↑a : α) ⇨ (↑b : α) = ((↑b : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
have rw : (↑a : α) ⇨ (↑b : α) = ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ
Tactic: rw [compl_sup, a.prop.eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
⊢ (↑a : α) ⇨ (↑b : α) = ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ
have refine : ∀ (c : α), c ⊓ (↑a : α) ≤ (↑b : α) ↔ c ≤ ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ
Tactic: refine eq_of_forall_le_iff fun c => le_himp_iff.trans ?_
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
c : α
⊢ c ⊓ (↑a : α) ≤ (↑b : α) ↔ c ≤ ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ
have rw : c ⊓ (↑a : α) ≤ (↑b : α) ↔ Disjoint (↑b : α)ᶜ (c ⊓ (↑a : α))
Tactic: rw [le_compl_iff_disjoint_right, disjoint_left_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Regular (goal)
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
c : α
⊢ c ⊓ (↑a : α) ≤ (↑b : α) ↔ Disjoint (↑b : α)ᶜ (c ⊓ (↑a : α))
have rw : c ⊓ (↑a : α) ≤ (↑b : α) ↔ c ⊓ (↑a : α) ≤ (↑b : α)
Tactic: rw [b.prop.disjoint_compl_left_iff]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : EquivLike F α β
inst_3 : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b ≤ a ↔ b ≤ (f : (a : α) → β) a
have h : b = (f : (a : α) → β) (EquivLike.inv f b)
Tactic: convert! (map_le_map_iff f).symm
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : EquivLike F α β
inst_3 : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b < a ↔ b < (f : (a : α) → β) a
have rw : LT.lt.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f b) : β) ((f : (a : α) → β) a : β) ↔ b < (f : (a : α) → β) a
Tactic: rw [← map_lt_map_iff f]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f g : α →o β
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : α → β) (monotone' : Monotone toFun)
  (h : { toFun := toFun, monotone' := monotone' : α →o β }.toFun = g.toFun),
  { toFun := toFun, monotone' := monotone' : α →o β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
g : α →o β
toFun : α → β
monotone' : Monotone toFun
h : { toFun := toFun, monotone' := monotone' : α →o β }.toFun = g.toFun
⊢ { toFun := toFun, monotone' := monotone' : α →o β } = g
have mk : ∀ (toFun_1 : α → β) (monotone'_1 : Monotone toFun_1)
  (h :
    { toFun := toFun, monotone' := monotone' : α →o β }.toFun =
      { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun),
  { toFun := toFun, monotone' := monotone' : α →o β } = { toFun := toFun_1, monotone' := monotone'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ f.comp id = f
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.comp id : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ comp id f = f
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((comp id f : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
⊢ Eq (α := α × β →o α × β) (OrderHom.prod fst snd) id
have h : ∀ (x : α) (y : β),
  Eq (α := α × β) ((OrderHom.prod fst snd : (a : α × β) → α × β) (x, y) : α × β)
    ((id : (a : α × β) → α × β) (x, y) : α × β)
Tactic: ext ⟨x, y⟩ : 2
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
f : α ↪o β
⊢ comp (id α) f = f
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((comp (id α) f : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
f : α ↪o β
⊢ f.comp (id β) = f
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.comp (id β) : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : α ↪o β
inst_2 : OrderBot α
inst_3 : OrderBot β
a₁ a₂ : α
h : Disjoint.{u_3} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a₂ : β)
x : α
h₁ : x ≤ a₁
h₂ : x ≤ a₂
⊢ x ≤ ⊥
have rw : ∀ (h₁ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₁ : β))
  (h₂ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₂ : β)),
  LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) ⊥ : β)
Tactic: rw [← f.le_iff_le] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ trans (refl α) e = e
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((trans (refl α) e : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ e.trans (refl β) = e
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e.trans (refl β) : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
Tactic: ext x