awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = 0 ↔ s = ∅
have refine_1 : ∀ (h : s.chainHeight r = 0), s = ∅
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
refine_1 : ∀ (h : s.chainHeight r = 0), s = ∅
⊢ s.chainHeight r = 0 ↔ s = ∅
have refine_2 : s = ∅ → s.chainHeight r = 0
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (hypothesis)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r = 0
⊢ s = ∅
have h₁ : ∀ a ⊆ s, IsChain r a → a = ∅
Tactic: simp only [chainHeight, iSup_eq_zero, encard_eq_zero, Subtype.forall, and_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ a ⊆ s, IsChain r a → a = ∅
⊢ s = ∅
have refine_1 : ∀ (x : α), x ∈ s ↔ Membership.mem (γ := Set α) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ 1 ≤ s.chainHeight r ↔ s.Nonempty
have mp : 1 ≤ s.chainHeight r → s.Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
mp : 1 ≤ s.chainHeight r → s.Nonempty
⊢ 1 ≤ s.chainHeight r ↔ s.Nonempty
have mpr : s.Nonempty → 1 ≤ s.chainHeight r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : 1 ≤ s.chainHeight r
⊢ s.Nonempty
have mp : ∀ (hh : s = ∅), False
Tactic: by_contra! hh
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.Nonempty
⊢ 1 ≤ s.chainHeight r
have mpr : ∀ (hh : s.chainHeight r < 1), False
Tactic: by_contra! hh
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
⊢ s.chainHeight r ≤ t.chainHeight r
have refine : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight r), (↑n : ℕ∞) ≤ t.chainHeight r
Tactic: refine forall_natCast_le_iff_le.mp fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
⊢ (↑n : ℕ∞) ≤ t.chainHeight r
have obtain : ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r a), (↑n : ℕ∞) ≤ t.chainHeight r
Tactic: obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight (flip r) = s.chainHeight r
have refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight (flip r)), (↑n : ℕ∞) ≤ s.chainHeight r
Tactic: refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight (flip r)), (↑n : ℕ∞) ≤ s.chainHeight r
⊢ s.chainHeight (flip r) = s.chainHeight r
have refine_2 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight r), (↑n : ℕ∞) ≤ s.chainHeight (flip r)
Tactic: refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight (flip r)
⊢ (↑n : ℕ∞) ≤ s.chainHeight r
have refine_1 : ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain (flip r) a), (↑n : ℕ∞) ≤ s.chainHeight r
Tactic: obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
⊢ (↑n : ℕ∞) ≤ s.chainHeight (flip r)
have refine_2 : ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r a), (↑n : ℕ∞) ≤ s.chainHeight (flip r)
Tactic: obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
⊢ chainHeight ((⇑e : (a : α) → β) '' s) r' = s.chainHeight r
have refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'), (↑n : ℕ∞) ≤ s.chainHeight r
Tactic: refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'), (↑n : ℕ∞) ≤ s.chainHeight r
⊢ chainHeight ((⇑e : (a : α) → β) '' s) r' = s.chainHeight r
have refine_2 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight r), (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
Tactic: refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
⊢ (↑n : ℕ∞) ≤ s.chainHeight r
have refine_1 : ∀ (a : Set β) (ha₁ : a ⊆ (⇑e : (a : α) → β) '' s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r' a),
  (↑n : ℕ∞) ≤ s.chainHeight r
Tactic: obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
a : Set β
ha₁ : a ⊆ (⇑e : (a : α) → β) '' s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r' a
⊢ (↑n : ℕ∞) ≤ s.chainHeight r
have refine_1 : encard.{u_1} (α := α) ((⇑e : (a : α) → β) ⁻¹' a) ≤ s.chainHeight r
Tactic: rw [← ha₂, ← Set.encard_preimage_of_injective_subset_range e.injective (by grind)]
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
⊢ (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
have refine_2 : ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r a),
  (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
Tactic: obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
⊢ (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
have refine_2 : encard.{u_2} (α := β) ((⇑e : (a : α) → β) '' a) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
Tactic: rw [← ha₂, ← e.injective.encard_image]
-- Lean 4 proof step from Mathlib.Order.Height (hypothesis)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ (chainHeight univ fun (x1 x2 : (↑s : Type u_1)) ↦ r (↑x1 : α) (↑x2 : α)) = s.chainHeight r
have 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)
Tactic: have hc := Set.chainHeight_eq_of_relEmbedding univ <| Subtype.relEmbedding (r · ·) (· ∈ s)
-- Lean 4 proof step from Mathlib.Order.Height (goal)
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 : α)
have h : ∀ (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: funext
-- Lean 4 proof step from Mathlib.Order.Height (hypothesis)
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)
⊢ (chainHeight univ fun (x1 x2 : (↑s : Type u_1)) ↦ r (↑x1 : α) (↑x2 : α)) = s.chainHeight r
have 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 : α)
Tactic: have hs : Subtype.val ⁻¹'o (r · ·) = (fun x y : s ↦ r x y) := by funext; simp
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c
have rw : a ⊓ b ≤ c ↔ b ⊓ a ≤ c
Tactic: rw [le_himp_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : a ⊓ b ≤ c ↔ b ⊓ a ≤ c
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c
have rw₁ : b ⊓ a ≤ c ↔ b ⊓ a ≤ c
Tactic: rw [le_himp_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ≤ a ⇨ c
have rw : a ⊓ b ≤ c ↔ b ≤ a ⇨ c
Tactic: rw [le_himp_iff, le_himp_iff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : a ⊓ b ≤ c ↔ b ≤ a ⇨ c
⊢ a ≤ b ⇨ c ↔ b ≤ a ⇨ c
have rw₁ : a ⊓ b ≤ c ↔ a ⊓ b ≤ c
Tactic: rw [le_himp_iff, le_himp_iff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ a ⇨ b ↔ a ≤ b
have rw : a ⊓ a ≤ b ↔ a ≤ b
Tactic: rw [le_himp_iff, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : a ⊓ a ≤ b ↔ a ≤ b
⊢ a ≤ a ⇨ b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [le_himp_iff, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ (a ⇨ b) ≤ b
have rw : (a ⇨ b) ⊓ a ≤ b
Tactic: rw [inf_comm, ← le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ b) ⊓ a ≤ b
⊢ a ⊓ (a ⇨ b) ≤ b
have rw₁ : a ⇨ b ≤ a ⇨ b
Tactic: rw [inf_comm, ← le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ a = b ⊓ a
have rw : a ⊓ (a ⇨ b) = b ⊓ a
Tactic: rw [inf_comm, inf_himp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : a ⊓ (a ⇨ b) = b ⊓ a
⊢ (a ⇨ b) ⊓ a = b ⊓ a
have rw₁ : a ⊓ b = b ⊓ a
Tactic: rw [inf_comm, inf_himp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : a ⊓ (a ⇨ b) = b ⊓ a
rw₁ : a ⊓ b = b ⊓ a
⊢ (a ⇨ b) ⊓ a = b ⊓ a
have rw₂ : b ⊓ a = b ⊓ a
Tactic: rw [inf_comm, inf_himp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇨ b = ⊤ ↔ a ≤ b
have rw : ⊤ ≤ a ⇨ b ↔ a ≤ b
Tactic: rw [← top_le_iff, le_himp_iff, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : ⊤ ≤ a ⇨ b ↔ a ≤ b
⊢ a ⇨ b = ⊤ ↔ a ≤ b
have rw₁ : ⊤ ⊓ a ≤ b ↔ a ≤ b
Tactic: rw [← top_le_iff, le_himp_iff, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : ⊤ ≤ a ⇨ b ↔ a ≤ b
rw₁ : ⊤ ⊓ a ≤ b ↔ a ≤ b
⊢ a ⇨ b = ⊤ ↔ a ≤ b
have rw₂ : a ≤ b ↔ a ≤ b
Tactic: rw [← top_le_iff, le_himp_iff, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ b ≤ ⊤ ⇨ a ↔ b ≤ a
have rw : b ⊓ ⊤ ≤ a ↔ b ≤ a
Tactic: rw [le_himp_iff, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : b ⊓ ⊤ ≤ a ↔ b ≤ a
⊢ b ≤ ⊤ ⇨ a ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [le_himp_iff, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c
have simp_rw : d ⊓ a ⊓ b ≤ c ↔ d ⊓ (a ⊓ b) ≤ c
Tactic: simp_rw [le_himp_iff, inf_assoc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
have rw : c ⊓ (b ⊓ a) ≤ c
Tactic: rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⇨ b ⇨ c = b ⇨ a ⇨ c
have simp_rw : a ⊓ b ⇨ c = b ⊓ a ⇨ c
Tactic: simp_rw [himp_himp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ b ⇨ a = b ⇨ a
have rw : b ⊓ b ⇨ a = b ⇨ a
Tactic: rw [himp_himp, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : b ⊓ b ⇨ a = b ⇨ a
⊢ b ⇨ b ⇨ a = b ⇨ a
have rw₁ : b ⇨ a = b ⇨ a
Tactic: rw [himp_himp, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
have simp_rw : d ⊓ a ≤ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
Tactic: simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
simp_rw : d ⊓ a ≤ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
have simp_rw₁ : d ⊓ a ≤ b ∧ d ⊓ a ≤ c ↔ d ≤ a ⇨ b ∧ d ≤ a ⇨ c
Tactic: simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⊔ b ⇨ c ↔ d ≤ (a ⇨ c) ⊓ (b ⇨ c)
have rw : a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
Tactic: rw [le_inf_iff, le_himp_comm, sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ a = b ⇨ a
have rw : (a ⇨ a) ⊓ (b ⇨ a) = b ⇨ a
Tactic: rw [sup_himp_distrib, himp_self, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ a) ⊓ (b ⇨ a) = b ⇨ a
⊢ a ⊔ b ⇨ a = b ⇨ a
have rw₁ : ⊤ ⊓ (b ⇨ a) = b ⇨ a
Tactic: rw [sup_himp_distrib, himp_self, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ a) ⊓ (b ⇨ a) = b ⇨ a
rw₁ : ⊤ ⊓ (b ⇨ a) = b ⇨ a
⊢ a ⊔ b ⇨ a = b ⇨ a
have rw₂ : b ⇨ a = b ⇨ a
Tactic: rw [sup_himp_distrib, himp_self, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ b = a ⇨ b
have rw : (a ⇨ b) ⊓ (b ⇨ b) = a ⇨ b
Tactic: rw [sup_himp_distrib, himp_self, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ b) ⊓ (b ⇨ b) = a ⇨ b
⊢ a ⊔ b ⇨ b = a ⇨ b
have rw₁ : (a ⇨ b) ⊓ ⊤ = a ⇨ b
Tactic: rw [sup_himp_distrib, himp_self, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : (a ⇨ b) ⊓ (b ⇨ b) = a ⇨ b
rw₁ : (a ⇨ b) ⊓ ⊤ = a ⇨ b
⊢ a ⊔ b ⇨ b = a ⇨ b
have rw₂ : a ⇨ b = a ⇨ b
Tactic: rw [sup_himp_distrib, himp_self, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
| a
have rw : ⊤ ⇨ a
Tactic: rw [← @top_himp _ _ a]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = a
have conv_rhs : b ⇨ a = ⊤ ⇨ a
Tactic: conv_rhs => rw [← @top_himp _ _ a]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a
have rw : b ⇨ a = a ⊔ b ⇨ a
Tactic: rw [← h.eq_top, sup_himp_self_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : b ⇨ a = a ⊔ b ⇨ a
⊢ b ⇨ a = ⊤ ⇨ a
have rw₁ : b ⇨ a = b ⇨ a
Tactic: rw [← h.eq_top, sup_himp_self_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ a ⇨ a ⊓ b = b
have rw : (a ⇨ a) ⊓ (a ⇨ b) = b
Tactic: rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (a ⇨ a) ⊓ (a ⇨ b) = b
⊢ a ⇨ a ⊓ b = b
have rw₁ : ⊤ ⊓ (a ⇨ b) = b
Tactic: rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (a ⇨ a) ⊓ (a ⇨ b) = b
rw₁ : ⊤ ⊓ (a ⇨ b) = b
⊢ a ⇨ a ⊓ b = b
have rw₂ : a ⇨ b = b
Tactic: rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
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
⊢ a ⇨ a ⊓ b = b
have rw₃ : b = b
Tactic: rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a ⊓ b = a
have rw : (b ⇨ a) ⊓ (b ⇨ b) = a
Tactic: rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (b ⇨ a) ⊓ (b ⇨ b) = a
⊢ b ⇨ a ⊓ b = a
have rw₁ : (b ⇨ a) ⊓ ⊤ = a
Tactic: rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (b ⇨ a) ⊓ (b ⇨ b) = a
rw₁ : (b ⇨ a) ⊓ ⊤ = a
⊢ b ⇨ a ⊓ b = a
have rw₂ : b ⇨ a = a
Tactic: rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
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
⊢ b ⇨ a ⊓ b = a
have rw₃ : a = a
Tactic: rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c
have rw : (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
Tactic: rw [le_himp_iff, inf_right_comm, ← le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
a_1 b_1 c_1 d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
have simp_rw : b ⊓ a ⊔ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a
Tactic: simp_rw [inf_comm a, ← le_himp_iff, sup_le_iff, le_himp_iff, ← sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
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 ≤ b ⊔ c
have rw : (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b
have rw : a ≤ b ⊔ c ↔ a ≤ c ⊔ b
Tactic: rw [sdiff_le_iff, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a ≤ b ⊔ c ↔ a ≤ c ⊔ b
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b
have rw₁ : a ≤ c ⊔ b ↔ a ≤ c ⊔ b
Tactic: rw [sdiff_le_iff, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ≤ c ↔ a \ c ≤ b
have rw : a ≤ b ⊔ c ↔ a \ c ≤ b
Tactic: rw [sdiff_le_iff, sdiff_le_iff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a ≤ b ⊔ c ↔ a \ c ≤ b
⊢ a \ b ≤ c ↔ a \ c ≤ b
have rw₁ : a ≤ b ⊔ c ↔ a ≤ b ⊔ c
Tactic: rw [sdiff_le_iff, sdiff_le_iff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b ≤ b ↔ a ≤ b
have rw : a ≤ b ⊔ b ↔ a ≤ b
Tactic: rw [sdiff_le_iff, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ≤ b ⊔ b ↔ a ≤ b
⊢ a \ b ≤ b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [sdiff_le_iff, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b
have rw : a ≤ b ⊔ a \ b
Tactic: rw [sup_comm, ← sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ≤ b ⊔ a \ b
⊢ a ≤ a \ b ⊔ b
have rw₁ : a \ b ≤ a \ b
Tactic: rw [sup_comm, ← sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ b \ a ⊔ a = b ⊔ a
have rw : a ⊔ b \ a = b ⊔ a
Tactic: rw [sup_comm, sup_sdiff_self, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ⊔ b \ a = b ⊔ a
⊢ b \ a ⊔ a = b ⊔ a
have rw₁ : a ⊔ b = b ⊔ a
Tactic: rw [sup_comm, sup_sdiff_self, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ⊔ b \ a = b ⊔ a
rw₁ : a ⊔ b = b ⊔ a
⊢ b \ a ⊔ a = b ⊔ a
have rw₂ : b ⊔ a = b ⊔ a
Tactic: rw [sup_comm, sup_sdiff_self, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ⊔ c \ a = c
have rw : b ⊔ c = c
Tactic: rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : b ⊔ c = c
⊢ b ⊔ c \ a = c
have rw₁ : c = c
Tactic: rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b ⊔ b = a
have rw : b ⊔ a \ b = a
Tactic: rw [sup_comm, sup_sdiff_cancel_right h]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
rw : b ⊔ a \ b = a
⊢ a \ b ⊔ b = a
have rw₁ : a = a
Tactic: rw [sup_comm, sup_sdiff_cancel_right h]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hac : c ≤ a
hbc : c ≤ b
h : a \ c = b \ c
⊢ a = b
have rw : a \ c ⊔ c = b
Tactic: rw [← sdiff_sup_cancel hac, h, sdiff_sup_cancel hbc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
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
⊢ a = b
have rw₁ : b \ c ⊔ c = b
Tactic: rw [← sdiff_sup_cancel hac, h, sdiff_sup_cancel hbc]