awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x z y : α
simp_rw : z ≤ x → (z ⊔ y) ⊓ x ≤ z ⊔ y ⊓ x
⊢ z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z

Tactic:
simp_rw [inf_comm x, sup_comm _ z]

Premises used: inf_comm, sup_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x z y : α
⊢ z ≤ x → (z ⊔ y) ⊓ x ≤ z ⊔ y ⊓ x

Tactic:
sup_inf_le_assoc_of_le y

Premises used: sup_inf_le_assoc_of_le
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x z y : α
⊢ z ≤ x → (z ⊔ y) ⊓ x ≤ z ⊔ y ⊓ x

Tactic:
exact sup_inf_le_assoc_of_le y

Premises used: sup_inf_le_assoc_of_le
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
h : x ≤ z
⊢ (x ⊔ y) ⊓ z = x ⊔ y ⊓ z

Tactic:
le_antisymm (sup_inf_le_assoc_of_le y h)
    (le_inf (sup_le_sup_left inf_le_left _) (sup_le h inf_le_right))

Premises used: sup_le_sup_left, inf_le_right, le_inf, le_antisymm, sup_inf_le_assoc_of_le, sup_le
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
⊢ x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z

Tactic:
(sup_inf_assoc_of_le y inf_le_right).symm

Premises used: inf_le_right, sup_inf_assoc_of_le, Eq.symm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : αᵒᵈ
xz : x ≤ z
rw : z ⊓ y ⊔ x = z ⊓ (y ⊔ x)
⊢ (x ⊔ y) ⊓ z = x ⊔ y ⊓ z

Tactic:
rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]

Premises used: eq_comm, inf_comm, sup_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : αᵒᵈ
xz : x ≤ z
⊢ z ⊓ y ⊔ x = z ⊓ (y ⊔ x)

Tactic:
@sup_inf_assoc_of_le α _ _ _ y _ xz

Premises used: sup_inf_assoc_of_le, OrderDual
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : αᵒᵈ
xz : x ≤ z
⊢ z ⊓ y ⊔ x = z ⊓ (y ⊔ x)

Tactic:
exact @sup_inf_assoc_of_le α _ _ _ y _ xz

Premises used: sup_inf_assoc_of_le
-- Module: Mathlib.Order.ModularLattice
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

Tactic:
hxy.antisymm ?_

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
refine : y ≤ x
⊢ x = y

Tactic:
refine hxy.antisymm ?_

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ x ⊔ z ⊓ y = y

Tactic:
rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup

Premises used: sup_inf_assoc_of_le, inf_eq_right
-- Module: Mathlib.Order.ModularLattice
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
rwa₂ : z ⊓ y ≤ x
rwa₃ rwa₄ rwa₅ rwa₆ : y ⊓ z ≤ x
⊢ y ≤ x

Tactic:
rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]

Premises used: Eq.le, and_iff_right, inf_comm, sup_le_iff, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x ⊓ z
hsup : y ⊔ z ≤ x ⊔ z
⊢ x = y

Tactic:
eq_of_le_of_inf_le_of_le_sup hxy (hinf.trans inf_le_left) (le_sup_left.trans hsup)

Premises used: le_sup_left, eq_of_le_of_inf_le_of_le_sup, inf_le_left, LE.le.trans
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z : α
hxy : y < x
hinf : x ⊓ z ≤ y ⊓ z
⊢ y ⊔ z < x ⊔ z

Tactic:
lt_of_le_of_ne (sup_le_sup_right (le_of_lt hxy) _) fun hsup =>
    ne_of_lt hxy <| eq_of_le_of_inf_le_of_sup_le (le_of_lt hxy) hinf (le_of_eq hsup.symm)

Premises used: sup_le_sup_right, le_of_lt, le_of_eq, Eq.symm, ne_of_lt, lt_of_le_of_ne, eq_of_le_of_inf_le_of_sup_le
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
z : α
⊢ StrictMono (β := α × α) fun (x : α) ↦ (x ⊓ z, x ⊔ z)

Tactic:
fun _x _y hxy ↦
  ⟨⟨inf_le_inf_right _ hxy.le, sup_le_sup_right hxy.le _⟩,
    fun ⟨inf_le, sup_le⟩ ↦ (sup_lt_sup_of_lt_of_inf_le_inf hxy inf_le).not_ge sup_le⟩

Premises used: False, StrictMono, sup_le_sup_right, sup_lt_sup_of_lt_of_inf_le_inf, LT.lt.le, inf_le_inf_right, _private.0.strictMono_inf_prod_sup.match_1, And.intro, LT.lt.not_ge
-- Module: Mathlib.Order.ModularLattice
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
simp : (A ⊓ K ≤ B ⊓ K ∧ A ⊔ K ≤ B ⊔ K) ∧ ¬(B ⊓ K ≤ A ⊓ K ∧ B ⊔ K ≤ A ⊔ K)
⊢ LT.lt (α := β × γ) ((fun (A : α) ↦ (f₂ A, g₂ A)) A) ((fun (A : α) ↦ (f₂ A, g₂ A)) B)

Tactic:
simp only [Prod.le_def, lt_iff_le_not_ge, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg]

Premises used: GaloisCoinsertion.l_le_l_iff, lt_iff_le_not_ge, GaloisInsertion.u_le_u_iff, Prod.le_def
-- Module: Mathlib.Order.ModularLattice
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
⊢ (A ⊓ K ≤ B ⊓ K ∧ A ⊔ K ≤ B ⊔ K) ∧ ¬(B ⊓ K ≤ A ⊓ K ∧ B ⊔ K ≤ A ⊔ K)

Tactic:
strictMono_inf_prod_sup hAB

Premises used: strictMono_inf_prod_sup
-- Module: Mathlib.Order.ModularLattice
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
⊢ (A ⊓ K ≤ B ⊓ K ∧ A ⊔ K ≤ B ⊔ K) ∧ ¬(B ⊓ K ≤ A ⊓ K ∧ B ⊔ K ≤ A ⊔ K)

Tactic:
exact strictMono_inf_prod_sup hAB

Premises used: strictMono_inf_prod_sup
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
β : Type u_2
γ : Type u_3
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : WellFoundedGT β
inst_5 : WellFoundedGT γ
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
⊢ WellFoundedGT α

Tactic:
wellFounded_lt_exact_sequence (α := αᵒᵈ) (β := γᵒᵈ) (γ := βᵒᵈ)
    K g₁ g₂ f₁ f₂ gi.dual gci.dual hg hf

Premises used: GaloisInsertion.dual, GaloisCoinsertion.dual, OrderDual, wellFounded_lt_exact_sequence
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc (a ⊓ b) a) : Type u_1)
change : a ⊓ ((↑x : α) ⊔ b) = (↑x : α)
⊢ (↑((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 : α)

Tactic:
change a ⊓ (↑x ⊔ b) = ↑x

Premises used: Max.max
-- Module: Mathlib.Order.ModularLattice
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 : α)
rw₂ rw₃ : (↑x : α) = (↑x : α)
⊢ a ⊓ ((↑x : α) ⊔ b) = (↑x : α)

Tactic:
rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1]

Premises used: Iff.mpr, inf_sup_assoc_of_le, sup_comm, And.right, And.left, sup_eq_right, Subtype.prop
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x_1 y z a b : α
x : (↑(Icc b (a ⊔ b)) : Type u_1)
change : a ⊓ (↑x : α) ⊔ b = (↑x : α)
⊢ (↑((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 : α)

Tactic:
change a ⊓ ↑x ⊔ b = ↑x
-- Module: Mathlib.Order.ModularLattice
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 : α)
rw₂ rw₃ : (↑x : α) = (↑x : α)
⊢ a ⊓ (↑x : α) ⊔ b = (↑x : α)

Tactic:
rw [inf_comm, inf_sup_assoc_of_le _ x.prop.1, inf_eq_left.2 x.prop.2]

Premises used: Iff.mpr, inf_sup_assoc_of_le, inf_comm, And.right, And.left, Subtype.prop, inf_eq_left
-- Module: Mathlib.Order.ModularLattice
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)
simp : (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ x ≤ y
⊢ 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

Tactic:
simp only [Subtype.mk_le_mk, Equiv.coe_fn_mk]

Premises used: Equiv.coe_fn_mk, Subtype.mk_le_mk
-- Module: Mathlib.Order.ModularLattice
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)
rw : (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ (↑x : α) ≤ (↑y : α)
⊢ (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ x ≤ y

Tactic:
rw [← Subtype.coe_le_coe]

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.Order.ModularLattice
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 : α)

Tactic:
⟨fun h => ?_, fun h => sup_le_sup_right h _⟩

Premises used: sup_le_sup_right, Iff.intro
-- Module: Mathlib.Order.ModularLattice
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)
refine : ∀ (h : (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b), (↑x : α) ≤ (↑y : α)
⊢ (↑x : α) ⊔ b ≤ (↑y : α) ⊔ b ↔ (↑x : α) ≤ (↑y : α)

Tactic:
refine ⟨fun h => ?_, fun h => sup_le_sup_right h _⟩
-- Module: Mathlib.Order.ModularLattice
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
rw : a ⊓ ((↑x : α) ⊔ b) ≤ a ⊓ ((↑y : α) ⊔ b)
⊢ (↑x : α) ≤ (↑y : α)

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]

Premises used: Iff.mpr, inf_sup_assoc_of_le, sup_comm, And.right, And.left, sup_eq_right, Subtype.prop
-- Module: Mathlib.Order.ModularLattice
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
⊢ a ⊓ ((↑x : α) ⊔ b) ≤ a ⊓ ((↑y : α) ⊔ b)

Tactic:
inf_le_inf_left _ h

Premises used: inf_le_inf_left
-- Module: Mathlib.Order.ModularLattice
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
⊢ a ⊓ ((↑x : α) ⊔ b) ≤ a ⊓ ((↑y : α) ⊔ b)

Tactic:
exact inf_le_inf_left _ h

Premises used: inf_le_inf_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
⊢ StrictMonoOn (β := α) (fun (c : α) ↦ a ⊓ c) (Icc b (a ⊔ b))

Tactic:
StrictMono.of_restrict (infIccOrderIsoIccSup a b).symm.strictMono

Premises used: OrderIso.strictMono, StrictMono.of_restrict, OrderIso.symm, infIccOrderIsoIccSup
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
⊢ StrictMonoOn (β := α) (fun (c : α) ↦ c ⊔ b) (Icc (a ⊓ b) a)

Tactic:
StrictMono.of_restrict (infIccOrderIsoIccSup a b).strictMono

Premises used: OrderIso.strictMono, StrictMono.of_restrict, infIccOrderIsoIccSup
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo (a ⊓ b) a) : Type u_1)
dsimp : a ⊓ ((↑c : α) ⊔ b) = (↑c : α)
⊢ (↑((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 : α)

Tactic:
dsimp
-- Module: Mathlib.Order.ModularLattice
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 : α)
rw₂ rw₃ : (↑c : α) = (↑c : α)
⊢ a ⊓ ((↑c : α) ⊔ b) = (↑c : α)

Tactic:
rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]

Premises used: Iff.mpr, inf_sup_assoc_of_le, LT.lt.le, sup_comm, And.right, And.left, sup_eq_right, Subtype.prop
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
c : (↑(Ioo b (a ⊔ b)) : Type u_1)
dsimp : a ⊓ (↑c : α) ⊔ b = (↑c : α)
⊢ (↑((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 : α)

Tactic:
dsimp
-- Module: Mathlib.Order.ModularLattice
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 : α)
rw₂ rw₃ : (↑c : α) = (↑c : α)
⊢ a ⊓ (↑c : α) ⊔ b = (↑c : α)

Tactic:
rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le]

Premises used: Iff.mpr, inf_sup_assoc_of_le, LT.lt.le, inf_comm, And.right, And.left, Subtype.prop, inf_eq_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
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)
⊢ a ⋖ a ⊔ b → a ⊓ b ⋖ b

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]

Premises used: Equiv.isEmpty_congr, right_lt_sup, Set.isEmpty_coe_sort, inf_comm, OrderIso.symm, inf_lt_left, sup_comm, infIooOrderIsoIooSup, RelIso.toEquiv, covBy_iff_Ioo_eq
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
⊢ ¬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:
id

Premises used: id
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
⊢ ¬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:
exact id

Premises used: id
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
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)
⊢ a ⊓ b ⋖ a → b ⋖ a ⊔ b

Tactic:
simp_rw [covBy_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
      (infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr]

Premises used: Equiv.isEmpty_congr, right_lt_sup, Set.isEmpty_coe_sort, inf_lt_left, infIooOrderIsoIooSup, RelIso.toEquiv, covBy_iff_Ioo_eq
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
⊢ ¬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:
id

Premises used: id
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x y z a b : α
⊢ ¬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:
exact id

Premises used: id
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₀ : Codisjoint a b
h₁ : Disjoint b c
h₂ : a ≤ c
⊢ c ≤ a

Tactic:
simpa [h₀.eq_top, h₁.eq_bot] using sup_inf_le_assoc_of_le b h₂

Premises used: sup_inf_le_assoc_of_le, Disjoint.eq_bot, Codisjoint.eq_top
-- Module: Mathlib.Order.ModularLattice
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
rw₁ rw₂ : (x ⊓ z ⊔ y) ⊓ z ≤ (x ⊓ z ⊔ y) ⊓ z
⊢ (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z

Tactic:
rw [← inf_eq_left.2 xz, h]

Premises used: Iff.mpr, inf_eq_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : DistribLattice α
x y z : α
xz : x ≤ z
rw : x ⊓ z ⊔ y ⊓ z ≤ x ⊔ y ⊓ z
rw₁ rw₂ : x ⊔ y ⊓ z ≤ x ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z

Tactic:
rw [inf_sup_right, inf_eq_left.2 xz]

Premises used: Iff.mpr, inf_sup_right, inf_eq_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
rw : a ⊓ (c ⊔ b) ≤ a ⊓ b
⊢ Disjoint a (b ⊔ c)

Tactic:
rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]

Premises used: sup_comm, disjoint_iff_inf_le, Disjoint.eq_bot
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
apply : a ⊓ (c ⊔ b) ≤ b
⊢ a ⊓ (c ⊔ b) ≤ a ⊓ b

Tactic:
apply le_inf inf_le_left

Premises used: le_inf, inf_le_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
apply : (b ⊔ a) ⊓ (c ⊔ b) ≤ b
apply₁ : α
⊢ a ⊓ (c ⊔ b) ≤ b

Tactic:
apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans

Premises used: le_sup_right, inf_le_inf_right, Max.max, LE.le.trans
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
rw : Disjoint c (b ⊔ a)
⊢ Disjoint (a ⊔ b) c

Tactic:
rw [disjoint_comm, sup_comm]

Premises used: disjoint_comm, sup_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
apply : Disjoint (c ⊔ b) a
⊢ Disjoint c (b ⊔ a)

Tactic:
apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm

Premises used: Disjoint.symm, Disjoint.disjoint_sup_right_of_disjoint_sup_left
-- Module: Mathlib.Order.ModularLattice
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hsup : Disjoint (c ⊔ b) a), Disjoint (c ⊔ b) a
⊢ Disjoint (c ⊔ b) a

Tactic:
rwa [sup_comm, disjoint_comm] at hsup

Premises used: disjoint_comm, sup_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (c ⊔ a)
rw : ∀ (h₂ : Disjoint b (a ⊔ c)), Disjoint c (b ⊔ a)
⊢ Disjoint c (a ⊔ b)

Tactic:
rw [sup_comm] at h₂ ⊢

Premises used: sup_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (a ⊔ c)
rw : Disjoint (b ⊔ a) c
⊢ Disjoint c (b ⊔ a)

Tactic:
rw [disjoint_comm]

Premises used: disjoint_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (a ⊔ c)
⊢ Disjoint (b ⊔ a) c

Tactic:
(h₁.mono_right le_sup_right).disjoint_sup_left_of_disjoint_sup_right h₂

Premises used: Disjoint.disjoint_sup_left_of_disjoint_sup_right, le_sup_right, Disjoint.mono_right
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (a ⊔ c)
⊢ Disjoint (b ⊔ a) c

Tactic:
exact (h₁.mono_right le_sup_right).disjoint_sup_left_of_disjoint_sup_right h₂

Premises used: Disjoint.disjoint_sup_left_of_disjoint_sup_right, le_sup_right, Disjoint.mono_right
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
h : Disjoint a b
hcomp : IsCompl (a ⊔ b) c
⊢ IsCompl a (b ⊔ c)

Tactic:
⟨h.disjoint_sup_right_of_disjoint_sup_left hcomp.disjoint, codisjoint_assoc.mp hcomp.codisjoint⟩

Premises used: codisjoint_assoc, Disjoint.disjoint_sup_right_of_disjoint_sup_left, Iff.mp, IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
h : Disjoint b c
hcomp : IsCompl a (b ⊔ c)
⊢ IsCompl (a ⊔ b) c

Tactic:
⟨h.disjoint_sup_left_of_disjoint_sup_right hcomp.disjoint, codisjoint_assoc.mpr hcomp.codisjoint⟩

Premises used: Iff.mpr, codisjoint_assoc, Disjoint.disjoint_sup_left_of_disjoint_sup_right, IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
disjoint :
  Disjoint (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })
codisjoint :
  Codisjoint (α := { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })
⊢ IsCompl (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })

Tactic:
constructor
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ Disjoint (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })

Tactic:
simp [disjoint_iff, Subtype.ext_iff, inf_comm a c, inf_assoc a, ← inf_assoc b, h₁.inf_eq_bot]

Premises used: disjoint_iff, inf_comm, Subtype.ext_iff, IsCompl.inf_eq_bot, inf_assoc