awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
s : LTSeries α
bl :
  s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
⊢ Membership.mem (γ := Finset (LTSeries α))
    (Finset.map (α :=
      { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) //
        StrictMono (f.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)) })
      (injStrictMono (Fintype.card α)) Finset.univ)
    s
have obtain : ∀ (l : ℕ) (f : Fin (l + 1) → α)
  (mf :
    ∀ (i : Fin l),
      Membership.mem (γ := SetRel α α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}
        (f i.castSucc, f i.succ))
  (bl :
    (RelSeries.mk (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            l f mf).length
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) <
      Fintype.card α),
  Membership.mem (γ := Finset (LTSeries α))
    (Finset.map (α :=
      { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) //
        StrictMono (f.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)) })
      (injStrictMono (Fintype.card α)) Finset.univ)
    (RelSeries.mk (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      l f mf)
Tactic: obtain ⟨l, f, mf⟩ := s
Cleared hypotheses: s, bl
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf :
  ∀ (i : Fin l),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (f i.castSucc, f i.succ)
bl :
  (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          l f mf).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
⊢ Membership.mem (γ := Finset (LTSeries α))
    (Finset.map (α :=
      { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) //
        StrictMono (f.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)) })
      (injStrictMono (Fintype.card α)) Finset.univ)
    (RelSeries.mk (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      l f mf)
have simp_rw : ∃ (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) (b :
  StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))),
  (injStrictMono (Fintype.card α) :
        (a : { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono f.snd }) → LTSeries α)
      (Subtype.mk (p := fun (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) ↦
        StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))) a b) =
    RelSeries.mk (r := {x : α × α | x.1 < x.2}) l f mf
Tactic: simp_rw [Finset.mem_map, Finset.mem_univ, true_and, Subtype.exists]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf :
  ∀ (i : Fin l),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (f i.castSucc, f i.succ)
bl :
  (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          l f mf).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
⊢ ∃ (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) (b :
    StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))),
    (injStrictMono (Fintype.card α) :
          (a : { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono f.snd }) → LTSeries α)
        (Subtype.mk (p := fun (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) ↦
          StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))) a b) =
      RelSeries.mk (r := {x : α × α | x.1 < x.2}) l f mf
have h : (injStrictMono (Fintype.card α) :
      (a : { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono f.snd }) → LTSeries α)
    (Subtype.mk (p := fun (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α) ⟨l, bl⟩ f) sorry) =
  RelSeries.mk (r := {x : α × α | x.1 < x.2}) l f mf
Tactic: use ⟨⟨l, bl⟩, f⟩, Fin.strictMono_iff_lt_succ.mpr mf
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)
have rw : ∀ (i : F) (j : i ∈ Y), LE.le.{u_3} (α := β) (⨅ x ∈ X, f x i) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)
Tactic: rw [iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, f x y) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)
have rw : ∀ (i : E) (j : i ∈ X), LE.le.{u_3} (α := β) (⨅ x ∈ X, f x y) (⨆ y ∈ Y, f i y)
Tactic: rw [le_iInf₂_iff]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
have refine_1 : ∀ (h : IsSaddlePointOn X Y f a b), ⨆ y ∈ Y, f a y = f a b
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, h'⟩ x hx y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
refine_1 : ∀ (h : IsSaddlePointOn X Y f a b), ⨆ y ∈ Y, f a y = f a b
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
have refine_2 : ∀ (h : IsSaddlePointOn X Y f a b), ⨅ x ∈ X, f x b = f a b
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, h'⟩ x hx y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
refine_1 : ∀ (h : IsSaddlePointOn X Y f a b), ⨆ y ∈ Y, f a y = f a b
refine_2 : ∀ (h : IsSaddlePointOn X Y f a b), ⨅ x ∈ X, f x b = f a b
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
have refine_3 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b →
  ∀ (x : E) (hx : x ∈ X) (y : F) (hy : y ∈ Y) (h : ⨆ y ∈ Y, f a y = f a b) (h' : ⨅ x ∈ X, f x b = f a b), f a y ≤ f x b
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, h'⟩ x hx y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y = f a b
have refine_1 : ⨆ y ∈ Y, f a y ≤ f a b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
refine_1 : ⨆ y ∈ Y, f a y ≤ f a b
⊢ ⨆ y ∈ Y, f a y = f a b
have refine_1₁ : f a b ≤ ⨆ y ∈ Y, f a y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y ≤ f a b
have refine_1 : ∀ (i : F) (i_1 : i ∈ Y), f a i ≤ f a b
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, f x b = f a b
have refine_2 : ⨅ x ∈ X, f x b ≤ f a b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
refine_2 : ⨅ x ∈ X, f x b ≤ f a b
⊢ ⨅ x ∈ X, f x b = f a b
have refine_2₁ : f a b ≤ ⨅ x ∈ X, f x b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ f a b ≤ ⨅ x ∈ X, f x b
have refine_2 : ∀ (i : E) (i_1 : i ∈ X), f a b ≤ f i b
Tactic: simp only [le_iInf_iff]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ f x b
have trans : f a y ≤ f a b
Tactic: trans f a b
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
trans : f a y ≤ f a b
⊢ f a y ≤ f x b
have trans₁ : f a b ≤ f x b
Tactic: trans f a b
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ f a b
have rw : f a y ≤ ⨆ y ∈ Y, f a y
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ f x b
have rw : ⨅ x ∈ X, f x b ≤ f x b
Tactic: rw [← h']
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
have rw : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
Tactic: rw [isSaddlePointOn_iff ha hb]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
have refine_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b →
  ∀ (h : ⨆ y ∈ Y, f a y = f a b) (h' : ⨅ x ∈ X, f x b = f a b), LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
Tactic: refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
refine_1 :
  ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b →
    ∀ (h : ⨆ y ∈ Y, f a y = f a b) (h' : ⨅ x ∈ X, f x b = f a b), LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
have refine_2 : ∀ (h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)), ⨆ y ∈ Y, f a y = f a b
Tactic: refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
refine_1 :
  ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b →
    ∀ (h : ⨆ y ∈ Y, f a y = f a b) (h' : ⨅ x ∈ X, f x b = f a b), LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
refine_2 : ∀ (h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)), ⨆ y ∈ Y, f a y = f a b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
have refine_3 : ∀ (h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)), ⨅ x ∈ X, f x b = f a b
Tactic: refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ ⨆ y ∈ Y, f a y = f a b
have refine_2 : ⨆ y ∈ Y, f a y ≤ f a b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
refine_2 : ⨆ y ∈ Y, f a y ≤ f a b
⊢ ⨆ y ∈ Y, f a y = f a b
have refine_2₁ : f a b ≤ ⨆ y ∈ Y, f a y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ ⨅ x ∈ X, f x b = f a b
have refine_3 : ⨅ x ∈ X, f x b ≤ f a b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
refine_3 : ⨅ x ∈ X, f x b ≤ f a b
⊢ ⨅ x ∈ X, f x b = f a b
have refine_3₁ : f a b ≤ ⨅ x ∈ X, f x b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (hypothesis)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
have h₁ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic: rw [isSaddlePointOn_iff ha hb] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
have left : ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
left : ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
have right : ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b
have left : ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ f a b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
left : ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b
have left₁ : f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ f a b
have left : LE.le.{u_3} (α := β) (⨅ x ∈ X, ⨆ y ∈ Y, f x y) (⨆ y ∈ Y, f a y)
Tactic: rw [← h.1]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
have left : LE.le.{u_3} (α := β) (⨅ x ∈ X, f x b) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)
Tactic: rw [← h.2]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, f x b) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)
have left : ∀ (i : E) (j : i ∈ X), f i b ≤ ⨆ y ∈ Y, f i y
Tactic: apply iInf₂_mono
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
have right : ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ f a b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
right : ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
have right₁ : f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ f a b
have right : LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨆ y ∈ Y, f a y)
Tactic: rw [← h.1]
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨆ y ∈ Y, f a y)
have right : ∀ (i : F) (j : i ∈ Y), ⨅ x ∈ X, f x i ≤ f a i
Tactic: apply iSup₂_mono
-- Lean 4 proof step from Mathlib.Order.SaddlePoint (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
have right : LE.le.{u_3} (α := β) (⨅ x ∈ X, f x b) (⨆ y ∈ Y, ⨅ x ∈ X, f x y)
Tactic: rw [← h.2]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
h : ScottContinuous f
x : Set α
d₁ : x.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) x
⊢ f (sSup x) = sSup (f '' x)
have rw : f (sSup x) = f (sSup x)
Tactic: rw [IsLUB.sSup_eq (h d₁ d₂ (isLUB_iff_sSup_eq.mpr rfl))]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x : Set α
d₁ : x.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) x
x_1 : α
hda : IsLUB x x_1
⊢ IsLUB (f '' x) (f x_1)
have rw : sSup (f '' x) = f x_1
Tactic: rw [isLUB_iff_sSup_eq, ← (h d₁ d₂), IsLUB.sSup_eq hda]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x : Set α
d₁ : x.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) x
x_1 : α
hda : IsLUB x x_1
rw : sSup (f '' x) = f x_1
⊢ IsLUB (f '' x) (f x_1)
have rw₁ : f (sSup x) = f x_1
Tactic: rw [isLUB_iff_sSup_eq, ← (h d₁ d₂), IsLUB.sSup_eq hda]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x : Set α
d₁ : x.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) x
x_1 : α
hda : IsLUB x x_1
rw : sSup (f '' x) = f x_1
rw₁ : f (sSup x) = f x_1
⊢ IsLUB (f '' x) (f x_1)
have rw₂ : f x_1 = f x_1
Tactic: rw [isLUB_iff_sSup_eq, ← (h d₁ d₂), IsLUB.sSup_eq hda]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
β : Type u_2
inst : CompleteLinearOrder β
a : β
d : Set β
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
⊢ min a (sSup d) = sSup ((fun (b : β) ↦ min a b) '' d)
have rw : Eq (α := β) (⨆ b ∈ d, min a b) (sSup ((fun (b : β) ↦ min a b) '' d))
Tactic: rw [inf_sSup_eq, sSup_image]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
β : Type u_2
inst : CompleteLinearOrder β
a : β
d : Set β
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
rw : Eq (α := β) (⨆ b ∈ d, min a b) (sSup ((fun (b : β) ↦ min a b) '' d))
⊢ min a (sSup d) = sSup ((fun (b : β) ↦ min a b) '' d)
have rw₁ : Eq.{u_2 + 1} (α := β) (⨆ b ∈ d, min a b) (⨆ a_1 ∈ d, min a a_1)
Tactic: rw [inf_sSup_eq, sSup_image]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
β : Type u_2
inst : CompleteLinearOrder β
b : β
d : Set β
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
⊢ min (sSup d) b = sSup ((fun (a : β) ↦ min a b) '' d)
have rw : Eq (α := β) (⨆ a ∈ d, min a b) (sSup ((fun (a : β) ↦ min a b) '' d))
Tactic: rw [sSup_inf_eq, sSup_image]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Complete (goal)
Goal:
β : Type u_2
inst : CompleteLinearOrder β
b : β
d : Set β
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
rw : Eq (α := β) (⨆ a ∈ d, min a b) (sSup ((fun (a : β) ↦ min a b) '' d))
⊢ min (sSup d) b = sSup ((fun (a : β) ↦ min a b) '' d)
have rw₁ : Eq.{u_2 + 1} (α := β) (⨆ a ∈ d, min a b) (⨆ a ∈ d, min a b)
Tactic: rw [sSup_inf_eq, sSup_image]