awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
inst : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
x_1 : (MultispanShape.prod ι).L
⊢ (match (motive := (MultispanShape.prod ι).L → T) x_1 with
    | (i, j) => v i j) ≤
    u ((MultispanShape.prod ι).snd x_1)

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
inst : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
i : (MultispanShape.prod ι).R
⊢ d.multispanIndex.right i ≤ x

Tactic:
grind [multispanIndex_right, le_iSup_iff]

Premises used: CompleteLattice.MulticoequalizerDiagram.multispanIndex_right, le_iSup_iff
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
inst : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
rw : (⨆ (i : Bool), bif i then x₃ else x₂) = x₂ ⊔ x₃
rw₁ : (⨆ (i : Bool), bif i then x₃ else x₂) = x₃ ⊔ x₂
rw₂ rw₃ : Eq.{u + 1} (α := T) (⨆ (i : Bool), bif i then x₃ else x₂) (⨆ (b : Bool), bif b then x₃ else x₂)
⊢ (⨆ (i : Bool), bif i then x₃ else x₂) = x₄

Tactic:
rw [← sq.sup_eq, sup_comm, sup_eq_iSup]

Premises used: sup_eq_iSup, Lattice.BicartSq.sup_eq, sup_comm
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
inst : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
i j : Bool
⊢ (bif i then bif j then x₃ else x₁ else bif j then x₁ else x₂) = (bif i then x₃ else x₂) ⊓ bif j then x₃ else x₂

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
⊢ sInf s i =
    ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i

Tactic:
simp [sInf, inf]

Premises used: _private.0.Pi.Lex.inf, InfSet.sInf
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
rw :
  ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i ≤
    e i
⊢ sInf s i ≤ e i

Tactic:
rw [sInf_apply]

Premises used: Pi.Lex.sInf_apply
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
⊢ ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i ≤
    e i

Tactic:
sInf_le ⟨⟨e, he, h⟩, rfl⟩

Premises used: iInf, Subtype.mk, sInf_le, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
⊢ ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i ≤
    e i

Tactic:
exact sInf_le ⟨⟨e, he, h⟩, rfl⟩
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
rw :
  e i ≤
    ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i
⊢ e i ≤ sInf s i

Tactic:
rw [sInf_apply]

Premises used: Pi.Lex.sInf_apply
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
h₁ :
  ∀ (b : (fun (i : ι) ↦ α i) i),
    Membership.mem (γ := Set ((fun (i : ι) ↦ α i) i))
        (Set.range
          fun
            (e :
              (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))) ↦
          (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i)
        b →
      e i ≤ b
⊢ e i ≤
    ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i

Tactic:
apply le_sInf

Premises used: le_sInf
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ ∀ (b : (fun (i : ι) ↦ α i) i),
    Membership.mem (γ := Set ((fun (i : ι) ↦ α i) i))
        (Set.range
          fun
            (e :
              (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))) ↦
          (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i)
        b →
      e i ≤ b

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsGLB s (sInf s)

Tactic:
⟨fun e he ↦ ?_, fun e h ↦ ?_⟩

Premises used: IsGreatest, IsGLB, And.intro
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
refine_1 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (he : e ∈ s), sInf s ≤ e
refine_2 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (h : e ∈ lowerBounds s), e ≤ sInf s
⊢ IsGLB s (sInf s)

Tactic:
refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
refine_1 : ∀ (hs : e < sInf s), False
⊢ sInf s ≤ e

Tactic:
by_contra! hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
hs : e < sInf s
refine_1 :
  ∀ (a : ι)
    (ha :
      (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sInf s j) ∧
        (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sInf s a)),
    False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sInf s j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sInf s a)
⊢ False

Tactic:
ha.2.not_ge (sInf_apply_le he ha.1)

Premises used: Pi.Lex.sInf_apply_le, And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sInf s j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sInf s a)
⊢ False

Tactic:
exact ha.2.not_ge (sInf_apply_le he ha.1)

Premises used: Pi.Lex.sInf_apply_le, And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
refine_2 : ∀ (hs : sInf s < e), False
⊢ e ≤ sInf s

Tactic:
by_contra! hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
hs : sInf s < e
refine_2 :
  ∀ (a : ι)
    (ha :
      (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sInf s j = e j) ∧
        (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sInf s a) (e a)),
    False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sInf s j = e j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sInf s a) (e a)
⊢ False

Tactic:
ha.2.not_ge <| le_sInf_apply fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_

Premises used: Pi.apply_le_of_toLex, Pi.Lex.le_sInf_apply, And.right, LT.lt.not_ge
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sInf s j = e j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sInf s a) (e a)
refine_2 :
  ∀ (f : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (hf : f ∈ s) (hf' : ∀ j < a, f j = sInf s j), ∀ j < a, e j = f j
⊢ False

Tactic:
refine ha.2.not_ge <| le_sInf_apply fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_

Premises used: Pi.apply_le_of_toLex, Pi.Lex.le_sInf_apply, And.right, LT.lt.not_ge
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sInf s j = e j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sInf s a) (e a)
f : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
hf : f ∈ s
hf' : ∀ j < a, f j = sInf s j
⊢ ∀ j < a, e j = f j

Tactic:
simp_all
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
⊢ sSup s i =
    ⨆ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sSup s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i

Tactic:
sInf_apply (α := fun i ↦ (α i)ᵒᵈ) ..

Premises used: Set.Mem, iSup, Lex, Pi.Lex.sInf_apply, setOf, OrderDual
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sSup s j
⊢ e i ≤ sSup s i

Tactic:
sInf_apply_le (α := fun i ↦ (α i)ᵒᵈ) he h

Premises used: Pi.Lex.sInf_apply_le
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sSup s j) → f i ≤ e i
⊢ sSup s i ≤ e i

Tactic:
le_sInf_apply (α := fun i ↦ (α i)ᵒᵈ) h

Premises used: Pi.Lex.le_sInf_apply
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsLUB s (sSup s)

Tactic:
⟨fun e he ↦ ?_, fun e h ↦ ?_⟩

Premises used: IsLeast, And.intro, IsLUB
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
refine_1 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (he : e ∈ s), e ≤ sSup s
refine_2 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (h : e ∈ upperBounds s), sSup s ≤ e
⊢ IsLUB s (sSup s)

Tactic:
refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
refine_1 : ∀ (hs : sSup s < e), False
⊢ e ≤ sSup s

Tactic:
by_contra! hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
hs : sSup s < e
refine_1 :
  ∀ (a : ι)
    (ha :
      (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sSup s j = e j) ∧
        (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sSup s a) (e a)),
    False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sSup s j = e j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sSup s a) (e a)
⊢ False

Tactic:
ha.2.not_ge (le_sSup_apply he fun j hj ↦ (ha.1 j hj).symm)

Premises used: And.right, And.left, LT.lt.not_ge, Pi.Lex.le_sSup_apply, Eq.symm
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sSup s j = e j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sSup s a) (e a)
⊢ False

Tactic:
exact ha.2.not_ge (le_sSup_apply he fun j hj ↦ (ha.1 j hj).symm)

Premises used: And.right, And.left, LT.lt.not_ge, Pi.Lex.le_sSup_apply, Eq.symm
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
refine_2 : ∀ (hs : e < sSup s), False
⊢ sSup s ≤ e

Tactic:
by_contra! hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
hs : e < sSup s
refine_2 :
  ∀ (a : ι)
    (ha :
      (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sSup s j) ∧
        (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sSup s a)),
    False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sSup s j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sSup s a)
⊢ False

Tactic:
ha.2.not_ge <| sSup_apply_le fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_

Premises used: Pi.Lex.sSup_apply_le, Pi.apply_le_of_toLex, And.right, LT.lt.not_ge
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sSup s j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sSup s a)
refine_2 :
  ∀ (f : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (hf : f ∈ s) (hf' : ∀ j < a, f j = sSup s j), ∀ j < a, f j = e j
⊢ False

Tactic:
refine ha.2.not_ge <| sSup_apply_le fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_

Premises used: Pi.Lex.sSup_apply_le, Pi.apply_le_of_toLex, And.right, LT.lt.not_ge
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sSup s j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sSup s a)
f : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
hf : f ∈ s
hf' : ∀ j < a, f j = sSup s j
⊢ ∀ j < a, f j = e j

Tactic:
simp_all
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
x : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsLUB x (sSup x)

Tactic:
isLUB_sSup

Premises used: Lex, _private.0.Pi.Lex.isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
x : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsLUB x (sSup x)

Tactic:
exact isLUB_sSup

Premises used: _private.0.Pi.Lex.isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
x : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsGLB x (sInf x)

Tactic:
isGLB_sInf

Premises used: Lex, _private.0.Pi.Lex.isGLB_sInf
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
x : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsGLB x (sInf x)

Tactic:
exact isGLB_sInf

Premises used: _private.0.Pi.Lex.isGLB_sInf
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
s : Set (Colex ((i : ι) → α i))
i : ι
⊢ sInf s i =
    ⨅ (e : (↑{e : Colex ((i : ι) → α i) | e ∈ s ∧ ∀ j > i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Colex ((i : ι) → α i)) i

Tactic:
Lex.sInf_apply (ι := ιᵒᵈ) s i

Premises used: Colex, Set.Mem, Pi.Lex.sInf_apply, setOf, OrderDual
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
s : Set (Colex ((i : ι) → α i))
i : ι
e : Colex ((i : ι) → α i)
he : e ∈ s
h : ∀ j > i, e j = sInf s j
⊢ sInf s i ≤ e i

Tactic:
Lex.sInf_apply_le (ι := ιᵒᵈ) he h

Premises used: Pi.Lex.sInf_apply_le
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
s : Set (Colex ((i : ι) → α i))
i : ι
e : Colex ((i : ι) → α i)
h : ∀ f ∈ s, (∀ j > i, f j = sInf s j) → e i ≤ f i
⊢ e i ≤ sInf s i

Tactic:
Lex.le_sInf_apply (ι := ιᵒᵈ) h

Premises used: Pi.Lex.le_sInf_apply
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
s : Set (Colex ((i : ι) → α i))
i : ι
⊢ sSup s i =
    ⨆ (e : (↑{e : Colex ((i : ι) → α i) | e ∈ s ∧ ∀ j > i, e j = sSup s j} : Type (max u_1 u_2))),
      (↑e : Colex ((i : ι) → α i)) i

Tactic:
Lex.sSup_apply (ι := ιᵒᵈ) s i

Premises used: Colex, Set.Mem, setOf, OrderDual, Pi.Lex.sSup_apply
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
s : Set (Colex ((i : ι) → α i))
i : ι
e : Colex ((i : ι) → α i)
he : e ∈ s
h : ∀ j > i, e j = sSup s j
⊢ e i ≤ sSup s i

Tactic:
Lex.le_sSup_apply (ι := ιᵒᵈ) he h

Premises used: Pi.Lex.le_sSup_apply
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
s : Set (Colex ((i : ι) → α i))
i : ι
e : Colex ((i : ι) → α i)
h : ∀ f ∈ s, (∀ j > i, f j = sSup s j) → f i ≤ e i
⊢ sSup s i ≤ e i

Tactic:
Lex.sSup_apply_le (ι := ιᵒᵈ) h

Premises used: Pi.Lex.sSup_apply_le
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
x : Set (Colex ((i : ι) → α i))
⊢ IsLUB x (sSup x)

Tactic:
Lex.isLUB_sSup (ι := ιᵒᵈ)

Premises used: Colex, OrderDual, _private.0.Pi.Lex.isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
x : Set (Colex ((i : ι) → α i))
⊢ IsLUB x (sSup x)

Tactic:
exact Lex.isLUB_sSup (ι := ιᵒᵈ)

Premises used: _private.0.Pi.Lex.isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
x : Set (Colex ((i : ι) → α i))
⊢ IsGLB x (sInf x)

Tactic:
Lex.isGLB_sInf (ι := ιᵒᵈ)

Premises used: Colex, _private.0.Pi.Lex.isGLB_sInf, OrderDual
-- Module: Mathlib.Order.CompleteLattice.PiLex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedGT ι
x : Set (Colex ((i : ι) → α i))
⊢ IsGLB x (sInf x)

Tactic:
exact Lex.isGLB_sInf (ι := ιᵒᵈ)

Premises used: _private.0.Pi.Lex.isGLB_sInf
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : Sublattice (Set X)
S T : ↥L
h : ∀ (x : X), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : Sublattice (Set X)
T : ↥L
x : X
⊢ Membership.mem (γ := Set X) ((L.subtype : (a : ↥L) → Set X) T : Set X) x ↔ x ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl