awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : (↑(Iio i) : Type u_6)) → PEquivOn (F := F) (X := X) f equivSucc (Iic (↑j : ι))
i_2 : ι
hj : i_2⁺ ∈ Iio i
k : (↑(Ioo i_2⁺ i) : Type u_6)
⊢ ∀ (hi : ¬IsMax i_2) (x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)),
    Eq.{u_8 + 1} (α :=
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 ⋯) :
          ι))
      (((↑(Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι)) ↦
                    Membership.mem (γ :=
                      Set ((l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι)))
                      (limit (F := piLT fun (j : ι) ↦ F j ≃ piLT X j) (piLTProj (X := fun (j : ι) ↦ F j ≃ piLT X j)) i)
                      x)
                    (fun (j : (↑(Iio i) : Type u_6)) ↦
                      PEquivOn.equiv (F := F) (X := X) (s := Iio (↑j : ι))
                        ((e j).restrict (F := F) (X := X) (s := Iio (↑j : ι)) (t := Iic (↑j : ι)) ⋯))
                    ⋯) :
                (l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι))
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι))
                (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι) ⋯) :
            (a : F (↑⟨i_2⁺, hj⟩ : ι)) → piLT X (↑⟨i_2⁺, hj⟩ : ι))
          x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 ⋯) :
        X
          (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 ⋯) :
            ι))
      (((equivSucc hi : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)

Tactic:
apply (e _).compat

Premises used: InverseSystem.PEquivOn.compat
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : (↑(Iio i) : Type u_6)) → PEquivOn (F := F) (X := X) f equivSucc (Iic (↑j : ι))
inst_4 : InverseSystem (F := F) f
equivLim : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7))
H :
  ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
    (↑((equivLim : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
i_2 : ι
hsj : i_2⁺ ∈ Iic i
hj : ¬IsMax i_2
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)
rw :
  Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((((pEquivOnGlue (F := F) (X := X) hi e).equiv (F := F) (X := X) (s := Iio i),
                equivLim.trans ((invLimEquiv (F := F) (X := X) ⋯).trans (Equiv.symm (piLTLim (X := X) hi)))).1
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ ⋯) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((piEquivLim (F := F) (X := X) ⋯ equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)

Tactic:
rw [piEquivLim, piSplitLE_lt (hi.succ_lt <| (succ_le_iff_of_not_isMax hj).mp hsj)]

Premises used: Order.succ_le_iff_of_not_isMax, InverseSystem.piSplitLE_lt, Order.IsSuccPrelimit.succ_lt, Iff.mp, InverseSystem.piEquivLim
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : (↑(Iio i) : Type u_6)) → PEquivOn (F := F) (X := X) f equivSucc (Iic (↑j : ι))
inst_4 : InverseSystem (F := F) f
equivLim : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7))
H :
  ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
    (↑((equivLim : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
i_2 : ι
hsj : i_2⁺ ∈ Iic i
hj : ¬IsMax i_2
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((((pEquivOnGlue (F := F) (X := X) hi e).equiv (F := F) (X := X) (s := Iio i),
                equivLim.trans ((invLimEquiv (F := F) (X := X) ⋯).trans (Equiv.symm (piLTLim (X := X) hi)))).1
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ ⋯) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)

Tactic:
apply (pEquivOnGlue hi e).compat

Premises used: InverseSystem.PEquivOn.compat, InverseSystem.pEquivOnGlue
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : WellFoundedLT ι
inst_2 : SuccOrder ι
inst_3 : InverseSystem (F := F) f
equivSucc :
  (i : ι) →
    ¬IsMax i → { e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i) // ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x }
equivLim :
  (i : ι) →
    IsSuccPrelimit i →
      { e : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7)) //
        ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
          (↑((e : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
            f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ Eq (α := piLT X i) ((globalEquiv (F := F) (X := X) equivSucc equivLim i : (a : F i) → piLT X i) (f h x) : piLT X i)
    (piLTProj (X := X) h ((globalEquiv (F := F) (X := X) equivSucc equivLim j : (a : F j) → piLT X j) x) : piLT X i)

Tactic:
(DFunLike.congr_fun ?_ _).trans ((globalEquivAux equivSucc equivLim j).nat le_rfl h h x)

Premises used: DFunLike.congr_fun, le_rfl, InverseSystem.PEquivOn.nat, _private.0.InverseSystem.globalEquivAux, Eq.trans
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : WellFoundedLT ι
inst_2 : SuccOrder ι
inst_3 : InverseSystem (F := F) f
equivSucc :
  (i : ι) →
    ¬IsMax i → { e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i) // ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x }
equivLim :
  (i : ι) →
    IsSuccPrelimit i →
      { e : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7)) //
        ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
          (↑((e : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
            f ⋯ x }
i j : ι
h : i ≤ j
x : F j
refine :
  globalEquiv (F := F) (X := X) equivSucc equivLim i =
    (globalEquivAux (F := F) (X := X) equivSucc equivLim j).equiv (F := F) (X := X) (s := Iic j)
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) i h)
⊢ Eq (α := piLT X i) ((globalEquiv (F := F) (X := X) equivSucc equivLim i : (a : F i) → piLT X i) (f h x) : piLT X i)
    (piLTProj (X := X) h ((globalEquiv (F := F) (X := X) equivSucc equivLim j : (a : F j) → piLT X j) x) : piLT X i)

Tactic:
refine (DFunLike.congr_fun ?_ _).trans ((globalEquivAux equivSucc equivLim j).nat le_rfl h h x)

Premises used: DFunLike.congr_fun, le_rfl, InverseSystem.PEquivOn.nat, _private.0.InverseSystem.globalEquivAux, Eq.trans
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : WellFoundedLT ι
inst_2 : SuccOrder ι
inst_3 : InverseSystem (F := F) f
equivSucc :
  (i : ι) →
    ¬IsMax i → { e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i) // ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x }
equivLim :
  (i : ι) →
    IsSuccPrelimit i →
      { e : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7)) //
        ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
          (↑((e : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
            f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ globalEquiv (F := F) (X := X) equivSucc equivLim i =
    (globalEquivAux (F := F) (X := X) equivSucc equivLim j).equiv (F := F) (X := X) (s := Iic j)
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) i h)

Tactic:
pEquivOn_apply_eq ((isLowerSet_Iic _).inter <| isLowerSet_Iic _)

Premises used: InverseSystem.globalEquiv, InverseSystem.pEquivOn_apply_eq, IsLowerSet.inter, isLowerSet_Iic
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : WellFoundedLT ι
inst_2 : SuccOrder ι
inst_3 : InverseSystem (F := F) f
equivSucc :
  (i : ι) →
    ¬IsMax i → { e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i) // ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x }
equivLim :
  (i : ι) →
    IsSuccPrelimit i →
      { e : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7)) //
        ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
          (↑((e : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
            f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ globalEquiv (F := F) (X := X) equivSucc equivLim i =
    (globalEquivAux (F := F) (X := X) equivSucc equivLim j).equiv (F := F) (X := X) (s := Iic j)
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) i h)

Tactic:
exact pEquivOn_apply_eq ((isLowerSet_Iic _).inter <| isLowerSet_Iic _)

Premises used: InverseSystem.pEquivOn_apply_eq, IsLowerSet.inter, isLowerSet_Iic
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : WellFoundedLT ι
inst_2 : SuccOrder ι
inst_3 : InverseSystem (F := F) f
equivSucc :
  (i : ι) →
    ¬IsMax i → { e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i) // ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x }
equivLim :
  (i : ι) →
    IsSuccPrelimit i →
      { e : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7)) //
        ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
          (↑((e : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
            f ⋯ x }
i : ι
hi : ¬IsMax i
x : F i⁺
⊢ Eq.{u_8 + 1} (α := X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i⁺) i ⋯) : ι))
    ((globalEquiv (F := F) (X := X) equivSucc equivLim i⁺ : (a : F i⁺) → piLT X i⁺) x
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i⁺) i ⋯) :
      X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i⁺) i ⋯) : ι))
    ((((↑(equivSucc i hi) : F i⁺ ≃ F i × X i) : (a : F i⁺) → F i × X i) x).2 : X i)

Tactic:
(globalEquivAux equivSucc equivLim i⁺).compat le_rfl hi x

Premises used: le_rfl, Order.succ, Set.Mem, InverseSystem.PEquivOn.compat, _private.0.InverseSystem.globalEquivAux
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
inst_2 : Subsingleton α
⊢ Disjoint a b

Tactic:
fun x _ _ ↦ le_of_eq (Subsingleton.elim x ⊥)

Premises used: Disjoint, Bot.bot, le_of_eq, Subsingleton.elim
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
⊢ Disjoint a b ↔ Disjoint b a

Tactic:
forall_congr' fun _ ↦ forall_comm

Premises used: Disjoint, forall_comm, forall_congr'
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
⊢ Disjoint a b → Disjoint b a

Tactic:
disjoint_comm.1

Premises used: disjoint_comm, Iff.mp
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
⊢ Symmetric.{u_1 + 1} (α := α) Disjoint

Tactic:
Disjoint.symm

Premises used: Symmetric, Disjoint.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a : α
⊢ Disjoint ⊥ a

Tactic:
fun _ hbot _ ↦ hbot

Premises used: Disjoint
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a : α
⊢ Disjoint a ⊥

Tactic:
fun _ _ hbot ↦ hbot

Premises used: Disjoint
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ Disjoint b d → Disjoint a c

Tactic:
fun h _ ha hc ↦ h (ha.trans h₁) (hc.trans h₂)

Premises used: Disjoint, LE.le.trans
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b c : α
h : a ≤ b
⊢ Disjoint b c → Disjoint a c

Tactic:
Disjoint.mono h le_rfl

Premises used: le_rfl, Disjoint.mono
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b c : α
h : b ≤ c
⊢ Disjoint a c → Disjoint a b

Tactic:
Disjoint.mono le_rfl h

Premises used: le_rfl, Disjoint.mono
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
h : Disjoint a b
x : α
h₁ : x ≤ a
h₂ : x ≤ b
⊢ x = ⊥

Tactic:
simpa using h h₁ h₂
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a : α
⊢ Disjoint a a ↔ a = ⊥

Tactic:
⟨fun hd ↦ bot_unique <| hd le_rfl le_rfl, fun h _ ha _ ↦ ha.trans_eq h⟩

Premises used: le_rfl, LE.le.trans_eq, Iff.intro, bot_unique
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
ha : a ≠ ⊥
hab : Disjoint a b
h : a = b
rwa rwa₁ rwa₂ rwa₃ : ∀ (hab : Disjoint a a) (h : a = b), Disjoint a a
⊢ Disjoint a a

Tactic:
rwa [← h] at hab
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
hab : Disjoint a b
h : a ≤ b
⊢ a = ⊥

Tactic:
eq_bot_iff.2 <| hab le_rfl h

Premises used: Iff.mpr, le_rfl, eq_bot_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
hab : Disjoint a b
⊢ b ≤ a → b = ⊥

Tactic:
hab.symm.eq_bot_of_le

Premises used: Disjoint.eq_bot_of_le, Disjoint.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
hab : Disjoint a b
⊢ a = b ↔ a = ⊥ ∧ b = ⊥

Tactic:
grind
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
hab : Disjoint a b
⊢ a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥

Tactic:
grind
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
h : a ≤ b
⊢ Disjoint a b ↔ a = ⊥

Tactic:
grind
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
a : α
⊢ Disjoint a ⊤ ↔ a = ⊥

Tactic:
⟨fun h ↦ bot_unique <| h le_rfl le_top, fun h _ ha _ ↦ ha.trans_eq h⟩

Premises used: le_rfl, LE.le.trans_eq, le_top, Iff.intro, bot_unique
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
a : α
⊢ Disjoint ⊤ a ↔ a = ⊥

Tactic:
⟨fun h ↦ bot_unique <| h le_top le_rfl, fun h _ _ ha ↦ ha.trans_eq h⟩

Premises used: le_rfl, LE.le.trans_eq, le_top, Iff.intro, bot_unique
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
a b : α
h : Disjoint a b
ha : a ≠ ⊥
⊢ b ≠ ⊤

Tactic:
grind
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
⊢ Disjoint a b ↔ a ⊓ b ≤ ⊥

Tactic:
⟨fun hd ↦ hd inf_le_left inf_le_right, fun h _ ha hb ↦ (le_inf ha hb).trans h⟩

Premises used: inf_le_right, le_inf, Iff.intro, inf_le_left, LE.le.trans
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
⊢ Disjoint a b ↔ a ⊓ b = ⊥

Tactic:
disjoint_iff_inf_le.trans le_bot_iff

Premises used: le_bot_iff, Iff.trans, disjoint_iff_inf_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this_1 : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf (P := pr) Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot (p := pr) hbot
rw : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = (↑⊥ : α)
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)

Tactic:
rw [disjoint_iff, disjoint_iff, ← Subtype.coe_inf Pinf, ← Subtype.coe_bot hbot]

Premises used: disjoint_iff, Subtype.coe_inf, Subtype.coe_bot
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this_1 : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf (P := pr) Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot (p := pr) hbot
⊢ a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = (↑⊥ : α)

Tactic:
Subtype.coe_inj.symm

Premises used: Subtype.coe_inj, Iff.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this_1 : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf (P := pr) Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot (p := pr) hbot
⊢ a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = (↑⊥ : α)

Tactic:
exact Subtype.coe_inj.symm

Premises used: Subtype.coe_inj, Iff.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
⊢ Disjoint a b → a ⊓ b ≤ ⊥

Tactic:
disjoint_iff_inf_le.mp

Premises used: Iff.mp, disjoint_iff_inf_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
⊢ Disjoint a b → a ⊓ b = ⊥

Tactic:
bot_unique ∘ Disjoint.le_bot

Premises used: Disjoint.le_bot, Function.comp, bot_unique
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)

Tactic:
grind [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
⊢ Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)

Tactic:
grind [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b

Tactic:
grind [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
h : Disjoint a b
⊢ Disjoint (a ⊓ c) b

Tactic:
h.mono_left inf_le_left

Premises used: Disjoint.mono_left, inf_le_left
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
h : Disjoint a b
⊢ Disjoint (c ⊓ a) b

Tactic:
h.mono_left inf_le_right

Premises used: inf_le_right, Disjoint.mono_left
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
h : Disjoint a b
⊢ Disjoint a (b ⊓ c)

Tactic:
h.mono_right inf_le_left

Premises used: inf_le_left, Disjoint.mono_right
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
h : Disjoint a b
⊢ Disjoint a (c ⊓ b)

Tactic:
h.mono_right inf_le_right

Premises used: inf_le_right, Disjoint.mono_right
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
h : Disjoint (a ⊓ b) c
hle : a ≤ c
⊢ Disjoint a b

Tactic:
disjoint_iff.2 <| h.eq_bot_of_le <| inf_le_of_left_le hle

Premises used: Iff.mpr, disjoint_iff, inf_le_of_left_le, Disjoint.eq_bot_of_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a b c : α
h : Disjoint (a ⊓ b) c
hle : b ≤ c
⊢ Disjoint a b

Tactic:
disjoint_iff.2 <| h.eq_bot_of_le <| inf_le_of_right_le hle

Premises used: Iff.mpr, inf_le_of_right_le, disjoint_iff, Disjoint.eq_bot_of_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a b : α
h : Disjoint a b
ha : a ≠ ⊥
⊢ b < a ⊔ b

Tactic:
le_sup_right.lt_of_ne fun eq ↦ ha (le_bot_iff.mp <| h le_rfl <| sup_eq_right.mp eq.symm)

Premises used: le_bot_iff, le_rfl, le_sup_right, LE.le.lt_of_ne, sup_eq_right, Iff.mp, Eq.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
a b c : α
⊢ Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c

Tactic:
simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]

Premises used: disjoint_iff, sup_eq_bot_iff, inf_sup_right
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
a b c : α
⊢ Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

Tactic:
simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]

Premises used: disjoint_iff, sup_eq_bot_iff, inf_sup_left
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ⊔ b) c

Tactic:
disjoint_sup_left.2 ⟨ha, hb⟩

Premises used: Iff.mpr, And.intro, disjoint_sup_left
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
a b c : α
hb : Disjoint a b
hc : Disjoint a c
⊢ Disjoint a (b ⊔ c)

Tactic:
disjoint_sup_right.2 ⟨hb, hc⟩

Premises used: Iff.mpr, disjoint_sup_right, And.intro
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
a b c : α
h : a ≤ b ⊔ c
hd : Disjoint a c
⊢ a ≤ b

Tactic:
le_of_inf_le_sup_le (le_trans hd.le_bot bot_le) <| sup_le h le_sup_right

Premises used: Disjoint.le_bot, le_sup_right, le_of_inf_le_sup_le, sup_le, bot_le, le_trans
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
a b c : α
h : a ≤ c ⊔ b
hd : Disjoint a c
rwa rwa₁ rwa₂ rwa₃ : a ≤ c ⊔ b
⊢ a ≤ b ⊔ c

Tactic:
rwa [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderTop α
a b c : α
⊢ Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c

Tactic:
simp only [codisjoint_iff, sup_inf_right, inf_eq_top_iff]

Premises used: codisjoint_iff, sup_inf_right, inf_eq_top_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderTop α
a b c : α
⊢ Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

Tactic:
simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]

Premises used: codisjoint_iff, sup_inf_left, inf_eq_top_iff