awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Heyting.Hom
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 : BiheytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ (a b : α), f' (a ⇨ b) = f' a ⇨ f' b

Tactic:
simpa only [h] using map_himp f

Premises used: HeytingHomClass.map_himp
-- Module: Mathlib.Order.Heyting.Hom
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 : BiheytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ (a b : α), f' (a \ b) = f' a \ f' b

Tactic:
simpa only [h] using map_sdiff f

Premises used: CoheytingHomClass.map_sdiff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
inst : BiheytingAlgebra α
inst_1 : BiheytingAlgebra β
f : BiheytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
ext fun _ => rfl

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

Tactic:
ext fun _ => rfl

Premises used: BiheytingHom.ext, rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BiheytingAlgebra α
inst_1 : BiheytingAlgebra β
inst_2 : BiheytingAlgebra γ
f : BiheytingHom α β
g₁ g₂ : BiheytingHom β γ
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, BiheytingHom.comp, BiheytingHom.ext, DFunLike.ext_iff, congr_arg, Iff.intro, Iff.mp
-- Module: Mathlib.Order.Heyting.Hom
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 : β) : γ)
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: BiheytingHom.comp_apply
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : Compl α
a : α
⊢ IsRegular a → aᶜᶜ = a

Tactic:
id

Premises used: Heyting.IsRegular, id
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) ⊥ᶜᶜ ⊥
rw₁ : Eq.{u_1 + 1} (α := α) ⊤ᶜ ⊥
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
⊢ IsRegular.{u_1} (α := α) ⊥

Tactic:
rw [IsRegular, compl_bot, compl_top]

Premises used: Heyting.IsRegular, compl_top, compl_bot
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) ⊤ᶜᶜ ⊤
rw₁ : Eq.{u_1 + 1} (α := α) ⊥ᶜ ⊤
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ IsRegular.{u_1} (α := α) ⊤

Tactic:
rw [IsRegular, compl_top, compl_bot]

Premises used: Heyting.IsRegular, compl_top, compl_bot
-- Module: Mathlib.Order.Heyting.Regular
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
rw₃ rw₄ : a ⊓ b = a ⊓ b
⊢ IsRegular (a ⊓ b)

Tactic:
rw [IsRegular, compl_compl_inf_distrib, ha.eq, hb.eq]

Premises used: Heyting.IsRegular.eq, Heyting.IsRegular, compl_compl_inf_distrib
-- Module: Mathlib.Order.Heyting.Regular
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
rw₃ rw₄ : a ⇨ b = a ⇨ b
⊢ IsRegular (a ⇨ b)

Tactic:
rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]

Premises used: Heyting.IsRegular.eq, Heyting.IsRegular, compl_compl_himp_distrib
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a : α
⊢ IsRegular aᶜ

Tactic:
compl_compl_compl _

Premises used: compl_compl_compl, Heyting.IsRegular
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
ha : IsRegular a
rw : b ≤ aᶜᶜ ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ Disjoint aᶜ b ↔ b ≤ a

Tactic:
rw [← le_compl_iff_disjoint_left, ha.eq]

Premises used: Heyting.IsRegular.eq, le_compl_iff_disjoint_left
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : α
hb : IsRegular b
rw : a ≤ bᶜᶜ ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ Disjoint a bᶜ ↔ a ≤ b

Tactic:
rw [← le_compl_iff_disjoint_right, hb.eq]

Premises used: Heyting.IsRegular.eq, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.Heyting.Regular
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} (α := α) ⊥ᶜ ⊤
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ a ⊔ aᶜ = ⊤

Tactic:
rw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]

Premises used: compl_sup, inf_compl_eq_bot, compl_bot
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
⊢ ∀ (a : Regular α), IsRegular (↑a : α)

Tactic:
Subtype.prop

Premises used: Heyting.Regular, Subtype.prop, Heyting.Regular.val
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := Regular α) val

Tactic:
Subtype.coe_injective

Premises used: Heyting.Regular, Subtype.coe_injective, Heyting.Regular.val
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : Regular α
⊢ (↑a : α) = (↑b : α) ↔ a = b

Tactic:
Subtype.coe_inj

Premises used: Subtype.coe_inj, Heyting.Regular, Heyting.Regular.val
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
⊢ Eq.{u_1 + 1} (α := α) (↑⊤ : α) ⊤

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
⊢ Eq.{u_1 + 1} (α := α) (↑⊥ : α) ⊥

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : Regular α
⊢ (↑(a ⊓ b) : α) = (↑a : α) ⊓ (↑b : α)

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : Regular α
⊢ (↑(a ⇨ b) : α) = (↑a : α) ⇨ (↑b : α)

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a : Regular α
⊢ (↑aᶜ : α) = (↑a : α)ᶜ

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : Regular α
⊢ (↑a : α) ≤ (↑b : α) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : Regular α
⊢ (↑a : α) < (↑b : α) ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a : α
⊢ (↑((toRegular : (a : α) → Regular α) a) : α) = aᶜᶜ

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a : Regular α
⊢ (toRegular : (a : α) → Regular α) (↑a : α) = a

Tactic:
coe_injective a.2

Premises used: Heyting.Regular.coe_injective, Subtype.property
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : Regular α
⊢ (↑(a ⊔ b) : α) = ((↑a : α) ⊔ (↑b : α))ᶜᶜ

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : Regular α
dsimp : ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ ((↑a : α) ⊔ (↑b : α) ⊓ (↑c : α))ᶜᶜ
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : α) ≤ (↑(a ⊔ b ⊓ c) : α)

Tactic:
dsimp
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : Regular α
rw : ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ (((↑a : α) ⊔ (↑b : α)) ⊓ ((↑a : α) ⊔ (↑c : α)))ᶜᶜ
rw₁ rw₂ : ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ
⊢ ((↑a : α) ⊔ (↑b : α))ᶜᶜ ⊓ ((↑a : α) ⊔ (↑c : α))ᶜᶜ ≤ ((↑a : α) ⊔ (↑b : α) ⊓ (↑c : α))ᶜᶜ

Tactic:
rw [sup_inf_left, compl_compl_inf_distrib]

Premises used: sup_inf_left, compl_compl_inf_distrib
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
a : Regular α
dsimp : ⊤ ≤ ((↑a : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
⊢ (↑⊤ : α) ≤ (↑(a ⊔ aᶜ) : α)

Tactic:
dsimp
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b : α
a : Regular α
rw : ⊤ ≤ ((↑a : α)ᶜ ⊓ (↑a : α)ᶜᶜ)ᶜ
rw₁ : LE.le.{u_1} (α := α) ⊤ ⊥ᶜ
rw₂ rw₃ : LE.le.{u_1} (α := α) ⊤ ⊤
⊢ ⊤ ≤ ((↑a : α) ⊔ (↑a : α)ᶜ)ᶜᶜ

Tactic:
rw [compl_sup, inf_compl_eq_bot, compl_bot]

Premises used: compl_sup, inf_compl_eq_bot, compl_bot
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
dsimp : (↑a : α) ⇨ (↑b : α) = ((↑b : α) ⊔ (↑a : α)ᶜ)ᶜᶜ
⊢ (↑(a ⇨ b) : α) = (↑(b ⊔ aᶜ) : α)

Tactic:
dsimp
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
rw : (↑a : α) ⇨ (↑b : α) = ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ
⊢ (↑a : α) ⇨ (↑b : α) = ((↑b : α) ⊔ (↑a : α)ᶜ)ᶜᶜ

Tactic:
rw [compl_sup, a.prop.eq]

Premises used: Heyting.IsRegular.eq, Heyting.Regular.prop, compl_sup
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
⊢ (↑a : α) ⇨ (↑b : α) = ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ

Tactic:
eq_of_forall_le_iff fun c => le_himp_iff.trans ?_

Premises used: le_himp_iff, Iff.trans, eq_of_forall_le_iff
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
refine : ∀ (c : α), c ⊓ (↑a : α) ≤ (↑b : α) ↔ c ≤ ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ
⊢ (↑a : α) ⇨ (↑b : α) = ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ

Tactic:
refine eq_of_forall_le_iff fun c => le_himp_iff.trans ?_

Premises used: le_himp_iff, Iff.trans, eq_of_forall_le_iff
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
c : α
rw : c ⊓ (↑a : α) ≤ (↑b : α) ↔ Disjoint (↑b : α)ᶜ (c ⊓ (↑a : α))
⊢ c ⊓ (↑a : α) ≤ (↑b : α) ↔ c ≤ ((↑b : α)ᶜ ⊓ (↑a : α))ᶜ

Tactic:
rw [le_compl_iff_disjoint_right, disjoint_left_comm]

Premises used: disjoint_left_comm, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a_1 b_1 : α
a b : Regular α
c : α
rw rw₁ : c ⊓ (↑a : α) ≤ (↑b : α) ↔ c ⊓ (↑a : α) ≤ (↑b : α)
⊢ c ⊓ (↑a : α) ≤ (↑b : α) ↔ Disjoint (↑b : α)ᶜ (c ⊓ (↑a : α))

Tactic:
rw [b.prop.disjoint_compl_left_iff]

Premises used: Heyting.Regular.prop, Heyting.IsRegular.disjoint_compl_left_iff
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : HeytingAlgebra α
a b : Regular α
⊢ (↑(a \ b) : α) = (↑a : α) ⊓ (↑b : α)ᶜ

Tactic:
rfl

Premises used: Heyting.Regular.val, rfl
-- Module: Mathlib.Order.Heyting.Regular
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ ∀ (a : α), IsRegular a

Tactic:
compl_compl

Premises used: compl_compl, Heyting.IsRegular
-- Module: Mathlib.Order.Heyting.Regular
Goal:
p : Prop
inst : Decidable p
⊢ IsRegular p

Tactic:
propext <| Decidable.not_not

Premises used: Heyting.IsRegular, propext, Decidable.not_not
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : LE α
inst_1 : LE β
x : (fun (x1 x2 : α) ↦ x1 ≤ x2) ↪r fun (x1 x2 : β) ↦ x1 ≤ x2
iso : α ↪ β
h rwa rwa₁ rwa₂ rwa₃ : ∀ (b a : α), LE.le.{u_7} (α := β) ((iso : (a : α) → β) b : β) ((iso : (a : α) → β) a : β) ↔ b ≤ a
⊢ ∀ {a b : α}, LE.le.{u_7} (α := β) ((iso : (a : α) → β) b : β) ((iso : (a : α) → β) a : β) ↔ b ≤ a

Tactic:
rwa [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : LE α
inst_1 : LE β
x : (fun (x1 x2 : α) ↦ x2 ≤ x1) ↪r fun (x1 x2 : β) ↦ x2 ≤ x1
iso : α ↪ β
h rwa rwa₁ rwa₂ rwa₃ : ∀ (b a : α), LE.le.{u_7} (α := β) ((iso : (a : α) → β) a : β) ((iso : (a : α) → β) b : β) ↔ a ≤ b
⊢ ∀ {a b : α}, LE.le.{u_7} (α := β) ((iso : (a : α) → β) a : β) ((iso : (a : α) → β) b : β) ↔ a ≤ b

Tactic:
rwa [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : LE α
inst_1 : LE β
x : (fun (x1 x2 : α) ↦ x1 ≤ x2) ≃r fun (x1 x2 : β) ↦ x1 ≤ x2
iso : α ≃ β
h rwa rwa₁ rwa₂ rwa₃ : ∀ (b a : α), LE.le.{u_7} (α := β) ((iso : (a : α) → β) b : β) ((iso : (a : α) → β) a : β) ↔ b ≤ a
⊢ ∀ {a b : α}, LE.le.{u_7} (α := β) ((iso : (a : α) → β) b : β) ((iso : (a : α) → β) a : β) ↔ b ≤ a

Tactic:
rwa [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : LE α
inst_1 : LE β
x : (fun (x1 x2 : α) ↦ x2 ≤ x1) ≃r fun (x1 x2 : β) ↦ x2 ≤ x1
iso : α ≃ β
h rwa rwa₁ rwa₂ rwa₃ : ∀ (b a : α), LE.le.{u_7} (α := β) ((iso : (a : α) → β) a : β) ((iso : (a : α) → β) b : β) ↔ a ≤ b
⊢ ∀ {a b : α}, LE.le.{u_7} (α := β) ((iso : (a : α) → β) a : β) ((iso : (a : α) → β) b : β) ↔ a ≤ b

Tactic:
rwa [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_6
α : Type u_7
β : Type u_8
inst : LE α
inst_1 : LE β
inst_2 : FunLike F α β
⊢ (RelHomClass.{u_6, u_7, u_8} F (α := α) (β := β) (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x1 x2 : β) ↦ x1 ≤ x2) =
    RelHomClass.{u_6, u_7, u_8} F (α := α) (β := β) (fun (x1 x2 : α) ↦ x2 ≤ x1) fun (x1 x2 : β) ↦ x2 ≤ x1

Tactic:
grind only [RelHomClass]

Premises used: RelHomClass
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : LE α
inst_1 : LE β
inst_2 : EquivLike F α β
inst_3 : OrderIsoClass F α β
⊢ OrderHomClass F α β

Tactic:
{ EquivLike.toEmbeddingLike (E := F) with
    map_rel := fun f _ _ => (map_le_map_iff f).2 }

Premises used: OrderIsoClass.map_le_map_iff, Iff.mpr, RelHomClass.mk, EquivLike.toEmbeddingLike
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : FunLike F α β
inst_3 : OrderHomClass F α β
f : F
⊢ Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
fun _ _ => map_rel f

Premises used: Monotone, RelHomClass.map_rel
-- Module: Mathlib.Order.Hom.Basic
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 ↔ LE.le.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f b) : β) ((f : (a : α) → β) a : β)

Tactic:
(map_le_map_iff f).symm

Premises used: OrderIsoClass.map_le_map_iff, Iff.symm
-- Module: Mathlib.Order.Hom.Basic
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 : β
h : b = (f : (a : α) → β) (EquivLike.inv f b)
⊢ EquivLike.inv f b ≤ a ↔ b ≤ (f : (a : α) → β) a

Tactic:
convert! (map_le_map_iff f).symm

Premises used: OrderIsoClass.map_le_map_iff, Iff.symm
-- Module: Mathlib.Order.Hom.Basic
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 : β
⊢ b = (f : (a : α) → β) (EquivLike.inv f b)

Tactic:
(EquivLike.right_inv f _).symm

Premises used: EquivLike.right_inv, Eq.symm
-- Module: Mathlib.Order.Hom.Basic
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 : β
⊢ b = (f : (a : α) → β) (EquivLike.inv f b)

Tactic:
exact (EquivLike.right_inv f _).symm

Premises used: EquivLike.right_inv, Eq.symm
-- Module: Mathlib.Order.Hom.Basic
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 ≤ EquivLike.inv f a ↔ b ≤ a

Tactic:
simp
-- Module: Mathlib.Order.Hom.Basic
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 : α
⊢ LT.lt.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a < b

Tactic:
lt_iff_lt_of_le_iff_le' (map_le_map_iff f) (map_le_map_iff f)

Premises used: OrderIsoClass.map_le_map_iff, lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Order.Hom.Basic
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 : β
rw :
  LT.lt.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f b) : β) ((f : (a : α) → β) a : β) ↔ b < (f : (a : α) → β) a
⊢ EquivLike.inv f b < a ↔ b < (f : (a : α) → β) a

Tactic:
rw [← map_lt_map_iff f]

Premises used: map_lt_map_iff
-- Module: Mathlib.Order.Hom.Basic
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 : β
⊢ LT.lt.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f b) : β) ((f : (a : α) → β) a : β) ↔ b < (f : (a : α) → β) a

Tactic:
simp only [EquivLike.apply_inv_apply]

Premises used: EquivLike.apply_inv_apply
-- Module: Mathlib.Order.Hom.Basic
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 < EquivLike.inv f a ↔ b < a

Tactic:
simp
-- Module: Mathlib.Order.Hom.Basic
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
mk :
  ∀ (toFun : α → β) (monotone' : Monotone toFun)
    (h : { toFun := toFun, monotone' := monotone' : α →o β }.toFun = g.toFun),
    { toFun := toFun, monotone' := monotone' : α →o β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Order.Hom.Basic
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
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 }
⊢ { toFun := toFun, monotone' := monotone' : α →o β } = g

Tactic:
cases g
-- Module: Mathlib.Order.Hom.Basic
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 δ
toFun : α → β
monotone' : Monotone toFun
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:
congr
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ (⇑{ toFun := f, monotone' := hf : α →o β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.monotone'

Premises used: OrderHom.monotone'
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.monotone

Premises used: OrderHom.monotone
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f g : α →o β
h : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
⊢ f = g

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ (↑f : α →o β) = f

Tactic:
rfl

Premises used: OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
F : Type u_6
inst_2 : FunLike F α β
inst_3 : OrderHomClass F α β
f : F
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →o β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl