awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β)
rw :
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) x : β)
⊢ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
have rw₁ : Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β)
Tactic: rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ (⇑f : (a : α) → β) '' s
⊢ x ∈ s ∩ preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y} ↔
    Minimal (fun (x : α) ↦ x ∈ s ∩ (⇑f : (a : α) → β) ⁻¹' t) x
have simp_rw : x ∈ s ∧
    Membership.mem (γ := Set α)
      (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y}) x ↔
  Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
Tactic: simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ (⇑f : (a : α) → β) '' s
simp_rw :
  x ∈ s ∧
      Membership.mem (γ := Set α)
        (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y}) x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
⊢ x ∈ s ∩ preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y} ↔
    Minimal (fun (x : α) ↦ x ∈ s ∩ (⇑f : (a : α) → β) ⁻¹' t) x
have simp_rw₁ : x ∈ s ∧ Membership.mem (γ := Set α) {a : α | Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) a : β)} x ↔
  Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
Tactic: simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ (⇑f : (a : α) → β) '' s
simp_rw :
  x ∈ s ∧
      Membership.mem (γ := Set α)
        (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y}) x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₁ :
  x ∈ s ∧
      Membership.mem (γ := Set α) {a : α | Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) a : β)} x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
⊢ x ∈ s ∩ preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y} ↔
    Minimal (fun (x : α) ↦ x ∈ s ∩ (⇑f : (a : α) → β) ⁻¹' t) x
have simp_rw₂ : x ∈ s ∧ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
  Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
Tactic: simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ (⇑f : (a : α) → β) '' s
simp_rw :
  x ∈ s ∧
      Membership.mem (γ := Set α)
        (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y}) x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₁ :
  x ∈ s ∧
      Membership.mem (γ := Set α) {a : α | Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) a : β)} x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₂ :
  x ∈ s ∧ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
⊢ x ∈ s ∩ preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y} ↔
    Minimal (fun (x : α) ↦ x ∈ s ∩ (⇑f : (a : α) → β) ⁻¹' t) x
have simp_rw₃ : x ∈ s ∧ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
  Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
Tactic: simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ (⇑f : (a : α) → β) '' s
simp_rw :
  x ∈ s ∧
      Membership.mem (γ := Set α)
        (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y}) x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₁ :
  x ∈ s ∧
      Membership.mem (γ := Set α) {a : α | Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) a : β)} x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₂ :
  x ∈ s ∧ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₃ :
  x ∈ s ∧ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
⊢ x ∈ s ∩ preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y} ↔
    Minimal (fun (x : α) ↦ x ∈ s ∩ (⇑f : (a : α) → β) ⁻¹' t) x
have simp_rw₄ : x ∈ s ∧ Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x ↔
  Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
Tactic: simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
P : α → Prop
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) {x : α | Minimal P x})
    {x : β | Minimal (fun (x : β) ↦ P ((f.symm : (a : β) → α) x)) x}
have h : ∀ (x x : β), P ((f.symm : (a : β) → α) x) ↔ ∃ (x₀ : α), P x₀ ∧ (f : (a : α) → β) x₀ = x
Tactic: convert! _root_.image_monotone_setOf_minimal (f := f) (by simp [f.le_iff_le])
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsWeakUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b
have rw : b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a
Tactic: rw [inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ b → a ⋖ a ⊔ b
have rw : b ⊓ a ⋖ b → a ⋖ b ⊔ a
Tactic: rw [sup_comm, inf_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x z y : α
⊢ z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z
have simp_rw : z ≤ x → (z ⊔ y) ⊓ x ≤ z ⊔ y ⊓ x
Tactic: simp_rw [inf_comm x, sup_comm _ z]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : αᵒᵈ
xz : x ≤ z
⊢ (x ⊔ y) ⊓ z = x ⊔ y ⊓ z
have rw : z ⊓ y ⊔ x = z ⊓ (y ⊔ x)
Tactic: rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ x = y
have refine : y ≤ x
Tactic: refine hxy.antisymm ?_
-- Lean 4 proof step from Mathlib.Order.ModularLattice (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ y ≤ x
have hsup₁ : x ⊔ z ⊓ y = y
Tactic: rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup
Cleared hypotheses: hsup
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
⊢ y ≤ x
have rwa : x ⊔ z ⊓ y ≤ x
Tactic: rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
rwa : x ⊔ z ⊓ y ≤ x
⊢ y ≤ x
have rwa₁ : x ≤ x ∧ z ⊓ y ≤ x
Tactic: rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
rwa : x ⊔ z ⊓ y ≤ x
rwa₁ : x ≤ x ∧ z ⊓ y ≤ x
⊢ y ≤ x
have rwa₂ : z ⊓ y ≤ x
Tactic: rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
β : Type u_2
γ : Type u_3
inst_2 : Preorder β
inst_3 : Preorder γ
h₁ : WellFoundedLT β
h₂ : WellFoundedLT γ
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ LT.lt (α := β × γ) ((fun (A : α) ↦ (f₂ A, g₂ A)) A) ((fun (A : α) ↦ (f₂ A, g₂ A)) B)
have simp : (A ⊓ K ≤ B ⊓ K ∧ A ⊔ K ≤ B ⊔ K) ∧ ¬(B ⊓ K ≤ A ⊓ K ∧ B ⊔ K ≤ A ⊔ K)
Tactic: simp only [Prod.le_def, lt_iff_le_not_ge, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc (a ⊓ b) a) : Type u_1)
⊢ (↑((fun (x : (↑(Icc b (a ⊔ b)) : Type u_1)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc (a ⊓ b) a) (a ⊓ (↑x : α)) ⋯ : { x : α // x ∈ Icc (a ⊓ b) a }))
          ((fun (x : (↑(Icc (a ⊓ b) a) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b (a ⊔ b)) ((↑x : α) ⊔ b) ⋯ : { x : α // x ∈ Icc b (a ⊔ b) }))
            x)) :
      α) =
    (↑x : α)
have change : a ⊓ ((↑x : α) ⊔ b) = (↑x : α)
Tactic: change a ⊓ (↑x ⊔ b) = ↑x
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc (a ⊓ b) a) : Type u_1)
⊢ a ⊓ ((↑x : α) ⊔ b) = (↑x : α)
have rw : a ⊓ (b ⊔ (↑x : α)) = (↑x : α)
Tactic: rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc (a ⊓ b) a) : Type u_1)
rw : a ⊓ (b ⊔ (↑x : α)) = (↑x : α)
⊢ a ⊓ ((↑x : α) ⊔ b) = (↑x : α)
have rw₁ : a ⊓ b ⊔ (↑x : α) = (↑x : α)
Tactic: rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc (a ⊓ b) a) : Type u_1)
rw : a ⊓ (b ⊔ (↑x : α)) = (↑x : α)
rw₁ : a ⊓ b ⊔ (↑x : α) = (↑x : α)
⊢ a ⊓ ((↑x : α) ⊔ b) = (↑x : α)
have rw₂ : (↑x : α) = (↑x : α)
Tactic: rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc b (a ⊔ b)) : Type u_1)
⊢ (↑((fun (x : (↑(Icc (a ⊓ b) a) : Type u_1)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b (a ⊔ b)) ((↑x : α) ⊔ b) ⋯ : { x : α // x ∈ Icc b (a ⊔ b) }))
          ((fun (x : (↑(Icc b (a ⊔ b)) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc (a ⊓ b) a) (a ⊓ (↑x : α)) ⋯ : { x : α // x ∈ Icc (a ⊓ b) a }))
            x)) :
      α) =
    (↑x : α)
have change : a ⊓ (↑x : α) ⊔ b = (↑x : α)
Tactic: change a ⊓ ↑x ⊔ b = ↑x
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc b (a ⊔ b)) : Type u_1)
⊢ a ⊓ (↑x : α) ⊔ b = (↑x : α)
have rw : (↑x : α) ⊓ a ⊔ b = (↑x : α)
Tactic: rw [inf_comm, inf_sup_assoc_of_le _ x.prop.1, inf_eq_left.2 x.prop.2]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc b (a ⊔ b)) : Type u_1)
rw : (↑x : α) ⊓ a ⊔ b = (↑x : α)
⊢ a ⊓ (↑x : α) ⊔ b = (↑x : α)
have rw₁ : (↑x : α) ⊓ (a ⊔ b) = (↑x : α)
Tactic: rw [inf_comm, inf_sup_assoc_of_le _ x.prop.1, inf_eq_left.2 x.prop.2]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc b (a ⊔ b)) : Type u_1)
rw : (↑x : α) ⊓ a ⊔ b = (↑x : α)
rw₁ : (↑x : α) ⊓ (a ⊔ b) = (↑x : α)
⊢ a ⊓ (↑x : α) ⊔ b = (↑x : α)
have rw₂ : (↑x : α) = (↑x : α)
Tactic: rw [inf_comm, inf_sup_assoc_of_le _ x.prop.1, inf_eq_left.2 x.prop.2]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y_1 z a b : α
x y : (↑(Icc (a ⊓ b) a) : Type u_1)
⊢ LE.le (α := (↑(Icc b (a ⊔ b)) : Type u_1))
      (({
              toFun := fun (x : (↑(Icc (a ⊓ b) a) : Type u_1)) ↦
                Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b (a ⊔ b)) ((↑x : α) ⊔ b) ⋯,
              invFun := fun (x : (↑(Icc b (a ⊔ b)) : Type u_1)) ↦
                Subtype.mk (p := fun (x : α) ↦ x ∈ Icc (a ⊓ b) a) (a ⊓ (↑x : α)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_1 : (↑(Icc (a ⊓ b) a) : Type u_1)) → (↑(Icc b (a ⊔ b)) : Type u_1))
          x :
        (↑(Icc b (a ⊔ b)) : Type u_1))
      (({
              toFun := fun (x : (↑(Icc (a ⊓ b) a) : Type u_1)) ↦
                Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b (a ⊔ b)) ((↑x : α) ⊔ b) ⋯,
              invFun := fun (x : (↑(Icc b (a ⊔ b)) : Type u_1)) ↦
                Subtype.mk (p := fun (x : α) ↦ x ∈ Icc (a ⊓ b) a) (a ⊓ (↑x : α)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_1 : (↑(Icc (a ⊓ b) a) : Type u_1)) → (↑(Icc b (a ⊔ b)) : Type u_1))
          y :
        (↑(Icc b (a ⊔ b)) : Type u_1)) ↔
    x ≤ y
have simp : (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ x ≤ y
Tactic: simp only [Subtype.mk_le_mk, Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y_1 z a b : α
x y : (↑(Icc (a ⊓ b) a) : Type u_1)
⊢ (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ x ≤ y
have rw : (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ (↑x : α) ≤ (↑y : α)
Tactic: rw [← Subtype.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y_1 z a b : α
x y : (↑(Icc (a ⊓ b) a) : Type u_1)
⊢ (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ (↑x : α) ≤ (↑y : α)
have refine : ∀ (h : (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b), (↑x : α) ≤ (↑y : α)
Tactic: refine ⟨fun h => ?_, fun h => sup_le_sup_right h _⟩
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y_1 z a b : α
x y : (↑(Icc (a ⊓ b) a) : Type u_1)
h : (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b
⊢ (↑x : α) ≤ (↑y : α)
have rw : a ⊓ ((↑x : α) ⊔ b) ≤ a ⊓ ((↑y : α) ⊔ b)
Tactic: rw [← sup_eq_right.2 x.prop.1, inf_sup_assoc_of_le _ x.prop.2, sup_comm, ←
      sup_eq_right.2 y.prop.1, inf_sup_assoc_of_le _ y.prop.2, sup_comm b]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo (a ⊓ b) a) : Type u_1)
⊢ (↑((fun (c : (↑(Ioo b (a ⊔ b)) : Type u_1)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ Ioo (a ⊓ b) a) (a ⊓ (↑c : α)) ⋯ : { x : α // x ∈ Ioo (a ⊓ b) a }))
          ((fun (c : (↑(Ioo (a ⊓ b) a) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ Ioo b (a ⊔ b)) ((↑c : α) ⊔ b) ⋯ : { x : α // x ∈ Ioo b (a ⊔ b) }))
            c)) :
      α) =
    (↑c : α)
have dsimp : a ⊓ ((↑c : α) ⊔ b) = (↑c : α)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo (a ⊓ b) a) : Type u_1)
⊢ a ⊓ ((↑c : α) ⊔ b) = (↑c : α)
have rw : a ⊓ (b ⊔ (↑c : α)) = (↑c : α)
Tactic: rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo (a ⊓ b) a) : Type u_1)
rw : a ⊓ (b ⊔ (↑c : α)) = (↑c : α)
⊢ a ⊓ ((↑c : α) ⊔ b) = (↑c : α)
have rw₁ : a ⊓ b ⊔ (↑c : α) = (↑c : α)
Tactic: rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo (a ⊓ b) a) : Type u_1)
rw : a ⊓ (b ⊔ (↑c : α)) = (↑c : α)
rw₁ : a ⊓ b ⊔ (↑c : α) = (↑c : α)
⊢ a ⊓ ((↑c : α) ⊔ b) = (↑c : α)
have rw₂ : (↑c : α) = (↑c : α)
Tactic: rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo b (a ⊔ b)) : Type u_1)
⊢ (↑((fun (c : (↑(Ioo (a ⊓ b) a) : Type u_1)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ Ioo b (a ⊔ b)) ((↑c : α) ⊔ b) ⋯ : { x : α // x ∈ Ioo b (a ⊔ b) }))
          ((fun (c : (↑(Ioo b (a ⊔ b)) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ Ioo (a ⊓ b) a) (a ⊓ (↑c : α)) ⋯ : { x : α // x ∈ Ioo (a ⊓ b) a }))
            c)) :
      α) =
    (↑c : α)
have dsimp : a ⊓ (↑c : α) ⊔ b = (↑c : α)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo b (a ⊔ b)) : Type u_1)
⊢ a ⊓ (↑c : α) ⊔ b = (↑c : α)
have rw : (↑c : α) ⊓ a ⊔ b = (↑c : α)
Tactic: rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo b (a ⊔ b)) : Type u_1)
rw : (↑c : α) ⊓ a ⊔ b = (↑c : α)
⊢ a ⊓ (↑c : α) ⊔ b = (↑c : α)
have rw₁ : (↑c : α) ⊓ (a ⊔ b) = (↑c : α)
Tactic: rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo b (a ⊔ b)) : Type u_1)
rw : (↑c : α) ⊓ a ⊔ b = (↑c : α)
rw₁ : (↑c : α) ⊓ (a ⊔ b) = (↑c : α)
⊢ a ⊓ (↑c : α) ⊔ b = (↑c : α)
have rw₂ : (↑c : α) = (↑c : α)
Tactic: rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
⊢ a ⋖ a ⊔ b → a ⊓ b ⋖ b
have simp_rw : ¬b ≤ a ∧ IsEmpty.{u_1 + 1} (↑(Ioo (b ⊓ a) b) : Type u_1) → ¬b ≤ a ∧ IsEmpty.{u_1 + 1} (↑(Ioo (b ⊓ a) b) : Type u_1)
Tactic: simp_rw [covBy_iff_Ioo_eq, sup_comm a, inf_comm a, ← isEmpty_coe_sort, right_lt_sup,
      inf_lt_left, (infIooOrderIsoIooSup b a).symm.toEquiv.isEmpty_congr]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
⊢ a ⊓ b ⋖ a → b ⋖ a ⊔ b
have simp_rw : ¬a ≤ b ∧ IsEmpty.{u_1 + 1} (↑(Ioo b (a ⊔ b)) : Type u_1) → ¬a ≤ b ∧ IsEmpty.{u_1 + 1} (↑(Ioo b (a ⊔ b)) : Type u_1)
Tactic: simp_rw [covBy_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
      (infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x y z : α
xz : x ≤ z
⊢ (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
have rw : (x ⊓ z ⊔ y) ⊓ z ≤ x ⊓ z ⊔ y ⊓ z
Tactic: rw [← inf_eq_left.2 xz, h]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x y z : α
xz : x ≤ z
rw : (x ⊓ z ⊔ y) ⊓ z ≤ x ⊓ z ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
have rw₁ : (x ⊓ z ⊔ y) ⊓ z ≤ (x ⊓ z ⊔ y) ⊓ z
Tactic: rw [← inf_eq_left.2 xz, h]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : DistribLattice α
x y z : α
xz : x ≤ z
⊢ (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
have rw : x ⊓ z ⊔ y ⊓ z ≤ x ⊔ y ⊓ z
Tactic: rw [inf_sup_right, inf_eq_left.2 xz]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : DistribLattice α
x y z : α
xz : x ≤ z
rw : x ⊓ z ⊔ y ⊓ z ≤ x ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
have rw₁ : x ⊔ y ⊓ z ≤ x ⊔ y ⊓ z
Tactic: rw [inf_sup_right, inf_eq_left.2 xz]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ Disjoint a (b ⊔ c)
have rw : a ⊓ (c ⊔ b) ≤ a ⊓ b
Tactic: rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ a ⊓ b
have apply : a ⊓ (c ⊔ b) ≤ b
Tactic: apply le_inf inf_le_left
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ b
have apply : (b ⊔ a) ⊓ (c ⊔ b) ≤ b
Tactic: apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (a ⊔ b) c
have rw : Disjoint c (b ⊔ a)
Tactic: rw [disjoint_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint c (b ⊔ a)
have apply : Disjoint (c ⊔ b) a
Tactic: apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a
have rwa : ∀ (hsup : Disjoint a (c ⊔ b)), Disjoint (c ⊔ b) a
Tactic: rwa [sup_comm, disjoint_comm] at hsup
Cleared hypotheses: hsup
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
rwa : ∀ (hsup : Disjoint a (c ⊔ b)), Disjoint (c ⊔ b) a
⊢ Disjoint (c ⊔ b) a
have rwa₁ : ∀ (hsup : Disjoint (c ⊔ b) a), Disjoint (c ⊔ b) a
Tactic: rwa [sup_comm, disjoint_comm] at hsup
Cleared hypotheses: hsup