awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
hc :
  (chainHeight
      (image (α := { x : α // x ∈ s })
        (⇑(Subtype.relEmbedding (fun (x1 x2 : α) ↦ r x1 x2) fun (x : α) ↦ x ∈ s) : (a : { x : α // x ∈ s }) → α) univ)
      fun (x1 x2 : α) ↦ r x1 x2) =
    chainHeight.{u_1} (α := { x : α // x ∈ s }) univ
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2)
x x_1 : { x : α // x ∈ s }
⊢ (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2) x x_1 = r (↑x : α) (↑x_1 : α)

Tactic:
simp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
hc :
  (chainHeight
      (image (α := { x : α // x ∈ s })
        (⇑(Subtype.relEmbedding (fun (x1 x2 : α) ↦ r x1 x2) fun (x : α) ↦ x ∈ s) : (a : { x : α // x ∈ s }) → α) univ)
      fun (x1 x2 : α) ↦ r x1 x2) =
    chainHeight.{u_1} (α := { x : α // x ∈ s }) univ
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2)
⊢ Eq.{u_1 + 1} (α := (x y : { x : α // x ∈ s }) → Prop)
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2) fun (x y : (↑s : Type u_1)) ↦
    r (↑x : α) (↑y : α)

Tactic:
have hs : Subtype.val ⁻¹'o (r · ·) = (fun x y : s ↦ r x y) := by funext; simp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
hc :
  (chainHeight
      (image (α := { x : α // x ∈ s })
        (⇑(Subtype.relEmbedding (fun (x1 x2 : α) ↦ r x1 x2) fun (x : α) ↦ x ∈ s) : (a : { x : α // x ∈ s }) → α) univ)
      fun (x1 x2 : α) ↦ r x1 x2) =
    chainHeight.{u_1} (α := { x : α // x ∈ s }) univ
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2)
hs :
  Eq.{u_1 + 1} (α := (x y : { x : α // x ∈ s }) → Prop)
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2) fun (x y : (↑s : Type u_1)) ↦
    r (↑x : α) (↑y : α)
⊢ (chainHeight univ fun (x1 x2 : (↑s : Type u_1)) ↦ r (↑x1 : α) (↑x2 : α)) = s.chainHeight r

Tactic:
simpa [hs] using hc.symm

Premises used: Eq.symm
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
inst : LE α
⊢ (chainHeight univ fun (x1 x2 : (↑s : Type u_1)) ↦ x1 ≤ x2) = s.chainHeight fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
simpa using chainHeight_coe_univ s (· ≤ ·)

Premises used: LE.le, Set.chainHeight_coe_univ
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
inst : LT α
⊢ (chainHeight univ fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = s.chainHeight fun (x1 x2 : α) ↦ x1 < x2

Tactic:
simpa using chainHeight_coe_univ s (· < ·)

Premises used: LT.lt, Set.chainHeight_coe_univ
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : HImp α
inst_1 : HImp β
a b : α × β
⊢ (a ⇨ b).fst = a.fst ⇨ b.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : HImp α
inst_1 : HImp β
a b : α × β
⊢ (a ⇨ b).snd = a.snd ⇨ b.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : HNot α
inst_1 : HNot β
a : α × β
⊢ (￢a).fst = ￢a.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : HNot α
inst_1 : HNot β
a : α × β
⊢ (￢a).snd = ￢a.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SDiff α
inst_1 : SDiff β
a b : α × β
⊢ (a \ b).fst = a.fst \ b.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SDiff α
inst_1 : SDiff β
a b : α × β
⊢ (a \ b).snd = a.snd \ b.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Compl α
inst_1 : Compl β
a : α × β
⊢ aᶜ.fst = a.fstᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Compl α
inst_1 : Compl β
a : α × β
⊢ aᶜ.snd = a.sndᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → HImp (π i)
a b : (i : ι) → π i
⊢ a ⇨ b = fun (i : ι) ↦ a i ⇨ b i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → HNot (π i)
a : (i : ι) → π i
⊢ ￢a = fun (i : ι) ↦ ￢a i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → HImp (π i)
a b : (i : ι) → π i
i : ι
⊢ (a ⇨ b) i = a i ⇨ b i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → HNot (π i)
a : (i : ι) → π i
i : ι
⊢ (￢a) i = ￢a i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
GeneralizedHeytingAlgebra.le_himp_iff _ _ _

Premises used: GeneralizedHeytingAlgebra.le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : a ⊓ b ≤ c ↔ b ⊓ a ≤ c
rw₁ rw₂ : b ⊓ a ≤ c ↔ b ⊓ a ≤ c
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c

Tactic:
rw [le_himp_iff, inf_comm]

Premises used: inf_comm, le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : a ⊓ b ≤ c ↔ b ≤ a ⇨ c
rw₁ rw₂ : a ⊓ b ≤ c ↔ a ⊓ b ≤ c
⊢ a ≤ b ⇨ c ↔ b ≤ a ⇨ c

Tactic:
rw [le_himp_iff, le_himp_iff']

Premises used: le_himp_iff', le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ b ⇨ a

Tactic:
le_himp_iff.2 inf_le_left

Premises used: Iff.mpr, le_himp_iff, inf_le_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : a ⊓ a ≤ b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a ≤ a ⇨ b ↔ a ≤ b

Tactic:
rw [le_himp_iff, inf_idem]

Premises used: le_himp_iff, inf_idem
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
⊢ a ⇨ a = ⊤

Tactic:
top_le_iff.1 <| le_himp_iff.2 inf_le_right

Premises used: Iff.mpr, inf_le_right, le_himp_iff, top_le_iff, Iff.mp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ a ≤ b

Tactic:
le_himp_iff.1 le_rfl

Premises used: le_rfl, le_himp_iff, Iff.mp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ b) ⊓ a ≤ b
rw₁ rw₂ : a ⇨ b ≤ a ⇨ b
⊢ a ⊓ (a ⇨ b) ≤ b

Tactic:
rw [inf_comm, ← le_himp_iff]

Premises used: inf_comm, le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : a ⊓ (a ⇨ b) = b ⊓ a
rw₁ : a ⊓ b = b ⊓ a
rw₂ rw₃ : b ⊓ a = b ⊓ a
⊢ (a ⇨ b) ⊓ a = b ⊓ a

Tactic:
rw [inf_comm, inf_himp, inf_comm]

Premises used: inf_comm, inf_himp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : ⊤ ≤ a ⇨ b ↔ a ≤ b
rw₁ : ⊤ ⊓ a ≤ b ↔ a ≤ b
rw₂ rw₃ : a ≤ b ↔ a ≤ b
⊢ a ⇨ b = ⊤ ↔ a ≤ b

Tactic:
rw [← top_le_iff, le_himp_iff, top_inf_eq]

Premises used: top_inf_eq, le_himp_iff, top_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
⊢ a ⇨ ⊤ = ⊤

Tactic:
himp_eq_top_iff.2 le_top

Premises used: Iff.mpr, himp_eq_top_iff, le_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : b ⊓ ⊤ ≤ a ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ b ≤ ⊤ ⇨ a ↔ b ≤ a

Tactic:
rw [le_himp_iff, inf_top_eq]

Premises used: inf_top_eq, le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
simp_rw : d ⊓ a ⊓ b ≤ c ↔ d ⊓ (a ⊓ b) ≤ c
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c

Tactic:
simp_rw [le_himp_iff, inf_assoc]

Premises used: le_himp_iff, inf_assoc
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : c ⊓ (b ⊓ a) ≤ c
⊢ b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

Tactic:
rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]

Premises used: le_himp_iff, himp_inf_self, inf_assoc
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ c ⊓ (b ⊓ a) ≤ c

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ c ⊓ (b ⊓ a) ≤ c

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

Tactic:
simpa using @himp_le_himp_himp_himp

Premises used: himp_le_himp_himp_himp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
simp_rw : a ⊓ b ⇨ c = b ⊓ a ⇨ c
⊢ a ⇨ b ⇨ c = b ⇨ a ⇨ c

Tactic:
simp_rw [himp_himp, inf_comm]

Premises used: himp_himp, inf_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : b ⊓ b ⇨ a = b ⇨ a
rw₁ rw₂ : b ⇨ a = b ⇨ a
⊢ b ⇨ b ⇨ a = b ⇨ a

Tactic:
rw [himp_himp, inf_idem]

Premises used: himp_himp, inf_idem
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
simp_rw : d ⊓ a ≤ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
simp_rw₁ : d ⊓ a ≤ b ∧ d ⊓ a ≤ c ↔ d ≤ a ⇨ b ∧ d ≤ a ⇨ c
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)

Tactic:
simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]

Premises used: le_inf_iff, le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
rw : a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
⊢ d ≤ a ⊔ b ⇨ c ↔ d ≤ (a ⇨ c) ⊓ (b ⇨ c)

Tactic:
rw [le_inf_iff, le_himp_comm, sup_le_iff]

Premises used: le_himp_comm, le_inf_iff, sup_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c

Tactic:
simp_rw [le_himp_comm]

Premises used: le_himp_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
h : a ≤ b
⊢ c ⇨ a ≤ c ⇨ b

Tactic:
le_himp_iff.2 <| himp_inf_le.trans h

Premises used: Iff.mpr, himp_inf_le, le_himp_iff, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
h : a ≤ b
⊢ b ⇨ c ≤ a ⇨ c

Tactic:
le_himp_iff.2 <| (inf_le_inf_left _ h).trans himp_inf_le

Premises used: Iff.mpr, himp_inf_le, inf_le_inf_left, le_himp_iff, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ b ⇨ c ≤ a ⇨ d

Tactic:
(himp_le_himp_right hab).trans <| himp_le_himp_left hcd

Premises used: himp_le_himp_right, himp_le_himp_left, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ a) ⊓ (b ⇨ a) = b ⇨ a
rw₁ : ⊤ ⊓ (b ⇨ a) = b ⇨ a
rw₂ rw₃ : b ⇨ a = b ⇨ a
⊢ a ⊔ b ⇨ a = b ⇨ a

Tactic:
rw [sup_himp_distrib, himp_self, top_inf_eq]

Premises used: top_inf_eq, himp_self, sup_himp_distrib
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ b) ⊓ (b ⇨ b) = a ⇨ b
rw₁ : (a ⇨ b) ⊓ ⊤ = a ⇨ b
rw₂ rw₃ : a ⇨ b = a ⇨ b
⊢ a ⊔ b ⇨ b = a ⇨ b

Tactic:
rw [sup_himp_distrib, himp_self, inf_top_eq]

Premises used: inf_top_eq, himp_self, sup_himp_distrib
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : ⊤ ⇨ a
| a

Tactic:
rw [← @top_himp _ _ a]

Premises used: top_himp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
conv_rhs : b ⇨ a = ⊤ ⇨ a
⊢ b ⇨ a = a

Tactic:
conv_rhs => rw [← @top_himp _ _ a]

Premises used: top_himp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : b ⇨ a = a ⊔ b ⇨ a
rw₁ rw₂ : b ⇨ a = b ⇨ a
⊢ b ⇨ a = ⊤ ⇨ a

Tactic:
rw [← h.eq_top, sup_himp_self_left]

Premises used: sup_himp_self_left, Codisjoint.eq_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ a ⇨ b = b

Tactic:
h.symm.himp_eq_right

Premises used: Codisjoint.himp_eq_right, Codisjoint.symm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (a ⇨ a) ⊓ (a ⇨ b) = b
rw₁ : ⊤ ⊓ (a ⇨ b) = b
rw₂ : a ⇨ b = b
rw₃ rw₄ : b = b
⊢ a ⇨ a ⊓ b = b

Tactic:
rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]

Premises used: himp_inf_distrib, Codisjoint.himp_eq_left, top_inf_eq, himp_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (b ⇨ a) ⊓ (b ⇨ b) = a
rw₁ : (b ⇨ a) ⊓ ⊤ = a
rw₂ : b ⇨ a = a
rw₃ rw₄ : a = a
⊢ b ⇨ a ⊓ b = a

Tactic:
rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]

Premises used: himp_inf_distrib, inf_top_eq, Codisjoint.himp_eq_right, himp_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
hac : Codisjoint a c
hba : b ≤ a
⊢ c ⇨ b ≤ a

Tactic:
(himp_le_himp_left hba).trans_eq hac.himp_eq_right

Premises used: LE.le.trans_eq, Codisjoint.himp_eq_right, himp_le_himp_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ (a ⇨ b) ⇨ b

Tactic:
le_himp_iff.2 inf_himp_le

Premises used: Iff.mpr, le_himp_iff, inf_himp_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ a = a ⇨ b ↔ a = b

Tactic:
simp [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ a ≠ a ⇨ b ↔ a ≠ b

Tactic:
himp_eq_himp_iff.not

Premises used: Iff.not, himp_eq_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

Tactic:
rw [le_himp_iff, inf_right_comm, ← le_himp_iff]

Premises used: le_himp_iff, inf_right_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c

Tactic:
himp_inf_le.trans le_himp_himp

Premises used: himp_inf_le, le_himp_himp, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c

Tactic:
exact himp_inf_le.trans le_himp_himp

Premises used: himp_inf_le, le_himp_himp, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
hba : b ≤ a
hcb : c ≤ b
⊢ (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c

Tactic:
(himp_triangle _ _ _).antisymm <| le_inf (himp_le_himp_left hcb) (himp_le_himp_right hba)

Premises used: himp_triangle, LE.le.antisymm, himp_le_himp_right, le_inf, himp_le_himp_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
⊢ GaloisConnection (fun (x : α) ↦ a ⊓ x) fun (x : α) ↦ a ⇨ x

Tactic:
fun _ _ ↦ Iff.symm le_himp_iff'

Premises used: le_himp_iff', Iff.symm, GaloisConnection
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
a_1 b_1 c_1 d a b c : α
simp_rw : b ⊓ a ⊔ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
simp_rw [inf_comm a, ← le_himp_iff, sup_le_iff, le_himp_iff, ← sup_le_iff]

Premises used: inf_comm, GeneralizedHeytingAlgebra.le_himp_iff, sup_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
a_1 b_1 c_1 d a b c : α
⊢ b ⊓ a ⊔ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a

Tactic:
rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
a_1 b_1 c_1 d : α
a b c : αᵒᵈ
rw : (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
a_1 b_1 c_1 d : α
a b c : αᵒᵈ
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b

Tactic:
le_himp_iff

Premises used: le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
a_1 b_1 c_1 d : α
a b c : αᵒᵈ
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b

Tactic:
exact le_himp_iff

Premises used: le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α_1
a b c d : α_1
α : ι → Type u_4
inst_1 : (i : ι) → GeneralizedHeytingAlgebra (α i)
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i ≤ b ⇨ c ↔ i ⊓ b ≤ c

Tactic:
simp [le_def]

Premises used: Pi.le_def
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c

Tactic:
GeneralizedCoheytingAlgebra.sdiff_le_iff _ _ _

Premises used: GeneralizedCoheytingAlgebra.sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a ≤ b ⊔ c ↔ a ≤ c ⊔ b
rw₁ rw₂ : a ≤ c ⊔ b ↔ a ≤ c ⊔ b
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b

Tactic:
rw [sdiff_le_iff, sup_comm]

Premises used: sup_comm, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a ≤ b ⊔ c ↔ a \ c ≤ b
rw₁ rw₂ : a ≤ b ⊔ c ↔ a ≤ b ⊔ c
⊢ a \ b ≤ c ↔ a \ c ≤ b

Tactic:
rw [sdiff_le_iff, sdiff_le_iff']

Premises used: sdiff_le_iff', sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b ≤ a

Tactic:
sdiff_le_iff.2 le_sup_right

Premises used: Iff.mpr, le_sup_right, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : Disjoint a b
⊢ Disjoint (a \ c) b

Tactic:
h.mono_left sdiff_le

Premises used: sdiff_le, Disjoint.mono_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : Disjoint a b
⊢ Disjoint a (b \ c)

Tactic:
h.mono_right sdiff_le

Premises used: sdiff_le, Disjoint.mono_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ≤ b ⊔ b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a \ b ≤ b ↔ a ≤ b

Tactic:
rw [sdiff_le_iff, sup_idem]

Premises used: sup_idem, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
⊢ a \ a = ⊥

Tactic:
le_bot_iff.1 <| sdiff_le_iff.2 le_sup_left

Premises used: le_bot_iff, Iff.mpr, le_sup_left, Iff.mp, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ b ⊔ a \ b

Tactic:
sdiff_le_iff.1 le_rfl

Premises used: le_rfl, Iff.mp, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ≤ b ⊔ a \ b
rw₁ rw₂ : a \ b ≤ a \ b
⊢ a ≤ a \ b ⊔ b

Tactic:
rw [sup_comm, ← sdiff_le_iff]

Premises used: sup_comm, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ a \ b = a

Tactic:
sup_of_le_left sdiff_le

Premises used: sdiff_le, sup_of_le_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b ⊔ a = a

Tactic:
sup_of_le_right sdiff_le

Premises used: sdiff_le, sup_of_le_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b ⊓ a = a \ b

Tactic:
inf_of_le_left sdiff_le

Premises used: inf_of_le_left, sdiff_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊓ a \ b = a \ b

Tactic:
inf_of_le_right sdiff_le

Premises used: inf_of_le_right, sdiff_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b \ a = a ⊔ b

Tactic:
le_antisymm (sup_le_sup_left sdiff_le _) (sup_le le_sup_left le_sup_sdiff)

Premises used: sup_le_sup_left, le_sup_left, le_sup_sdiff, sdiff_le, le_antisymm, sup_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ⊔ b \ a = b ⊔ a
rw₁ : a ⊔ b = b ⊔ a
rw₂ rw₃ : b ⊔ a = b ⊔ a
⊢ b \ a ⊔ a = b ⊔ a

Tactic:
rw [sup_comm, sup_sdiff_self, sup_comm]

Premises used: sup_comm, sup_sdiff_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : c ≤ a
⊢ a ⊔ b \ c = a ⊔ b

Tactic:
sup_congr_left (sdiff_le.trans le_sup_right) <| le_sup_sdiff.trans <| sup_le_sup_right h _

Premises used: sup_le_sup_right, le_sup_sdiff, le_sup_right, sdiff_le, sup_congr_left, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : b ⊔ c = c
rw₁ rw₂ : c = c
⊢ b ⊔ c \ a = c

Tactic:
rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]

Premises used: sup_of_le_right, sup_sdiff_eq_sup
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
⊢ a ⊔ b \ a = b

Tactic:
sup_sdiff_cancel' le_rfl h

Premises used: le_rfl, sup_sdiff_cancel'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
rw : b ⊔ a \ b = a
rw₁ rw₂ : a = a
⊢ a \ b ⊔ b = a

Tactic:
rw [sup_comm, sup_sdiff_cancel_right h]

Premises used: sup_sdiff_cancel_right, sup_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hac : c ≤ a
hbc : c ≤ b
h : a \ c = b \ c
rw : a \ c ⊔ c = b
rw₁ : b \ c ⊔ c = b
rw₂ rw₃ : b = b
⊢ a = b

Tactic:
rw [← sdiff_sup_cancel hac, h, sdiff_sup_cancel hbc]

Premises used: sdiff_sup_cancel
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : b ≤ c \ a
hac : a ≤ c
⊢ a ⊔ b ≤ c

Tactic:
sup_le hac <| h.trans sdiff_le

Premises used: sdiff_le, sup_le, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : a ≤ c \ b
hbc : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
sup_le (h.trans sdiff_le) hbc

Premises used: sdiff_le, sup_le, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ b ≤ ⊥ ↔ a ≤ b
rw₁ : a ≤ b ⊔ ⊥ ↔ a ≤ b
rw₂ rw₃ : a ≤ b ↔ a ≤ b
⊢ a \ b = ⊥ ↔ a ≤ b

Tactic:
rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]

Premises used: le_bot_iff, sup_bot_eq, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ≤ ⊥ ⊔ b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a \ ⊥ ≤ b ↔ a ≤ b

Tactic:
rw [sdiff_le_iff, bot_sup_eq]

Premises used: bot_sup_eq, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
⊢ ⊥ \ a = ⊥

Tactic:
sdiff_eq_bot_iff.2 bot_le

Premises used: Iff.mpr, sdiff_eq_bot_iff, bot_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a ≤ a ⊔ (b ⊔ c)
⊢ (a \ b) \ (a \ c) ≤ c \ b

Tactic:
rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self,
    sup_left_comm]

Premises used: sdiff_sup_self, sup_left_comm, sdiff_le_iff, sup_sdiff_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a ⊔ (b ⊔ c)

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a ⊔ (b ⊔ c)

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a \ c ⊔ c \ b)

Tactic:
simpa using @sdiff_sdiff_sdiff_le_sdiff

Premises used: sdiff_sdiff_sdiff_le_sdiff