awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (hij : r i j),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
have inr : ∀ (b : α i),
  Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
Cleared hypotheses: j, b
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (hij : r i j),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
inr :
  ∀ (b : α i),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
have inr₁ : ∀ (hji : r j i),
  Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
have inr : ∀ (hab : s i a b),
  Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
Tactic: obtain hab | rfl | hba := trichotomous_of (s i) a b
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
inr :
  ∀ (hab : s i a b),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
have inr₁ : Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a) ∨
  mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i a ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a)
Tactic: obtain hab | rfl | hba := trichotomous_of (s i) a b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
inr :
  ∀ (hab : s i a b),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
inr₁ :
  Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i a ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
have inr₂ : ∀ (hba : s i b a),
  Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
Tactic: obtain hab | rfl | hba := trichotomous_of (s i) a b
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex (β := α) r s a b ↔
    r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (b.fst (β := fun (i : ι) ↦ α i))
          (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ α i))
have mp : Lex (β := α) r s a b →
  r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      s (b.fst (β := fun (i : ι) ↦ α i))
        (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          (a.snd (β := fun (i : ι) ↦ α i)) h)
        (b.snd (β := fun (i : ι) ↦ α i))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
mp :
  Lex (β := α) r s a b →
    r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (b.fst (β := fun (i : ι) ↦ α i))
          (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ α i))
⊢ Lex (β := α) r s a b ↔
    r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (b.fst (β := fun (i : ι) ↦ α i))
          (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ α i))
have mpr : (r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      s (b.fst (β := fun (i : ι) ↦ α i))
        (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          (a.snd (β := fun (i : ι) ↦ α i)) h)
        (b.snd (β := fun (i : ι) ↦ α i))) →
  Lex (β := α) r s a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (b.fst (β := fun (i : ι) ↦ α i))
          (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ α i))) →
    Lex (β := α) r s a b
have mpr : ∀ (i : ι) (a : α i),
  (r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (b.fst (β := fun (i : ι) ↦ α i))
          (Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦
            α x) ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ α i))) →
    Lex (β := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b
Tactic: obtain ⟨i, a⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
⊢ (r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (b.fst (β := fun (i : ι) ↦ α i))
          (Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦
            α x) ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ α i))) →
    Lex (β := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b
have mpr : (r i (b.fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h : i = b.fst (β := fun (i : ι) ↦ α i)),
      s (b.fst (β := fun (i : ι) ↦ α i)) (Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ α x) a h)
        (b.snd (β := fun (i : ι) ↦ α i))) →
  Lex (β := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex (β := α) r₁ s₁ a b
⊢ Lex (β := α) r₂ s₂ a b
have left : ∀ {a₁ : ι} (a : α a₁) {a₂ : ι} (b : α a₂) (hij : r₁ a₁ a₂), Lex (β := α) r₂ s₂ (mk (β := α) a₁ a) (mk (β := α) a₂ b)
Tactic: obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.Data.Sigma.Lex (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex (β := α) r₁ s₁ a b
left :
  ∀ {a₁ : ι} (a : α a₁) {a₂ : ι} (b : α a₂) (hij : r₁ a₁ a₂), Lex (β := α) r₂ s₂ (mk (β := α) a₁ a) (mk (β := α) a₂ b)
⊢ Lex (β := α) r₂ s₂ a b
have right : ∀ (i : ι) {b₁ b₂ : α i} (hab : s₁ i b₁ b₂), Lex (β := α) r₂ s₂ (mk (β := α) i b₁) (mk (β := α) i b₂)
Tactic: obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)
have mp : a ≤ b →
  ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i)) h ≤
      b.snd (β := fun (i : ι) ↦ α i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
a b : (i : ι) × α i
mp :
  a ≤ b →
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)
⊢ a ≤ b ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)
have mpr : (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i)) h ≤
      b.snd (β := fun (i : ι) ↦ α i)) →
  a ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)) →
    a ≤ b
have mpr : ∀ (i : ι) (a : α i),
  (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
        b.snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a ≤ b
Tactic: obtain ⟨i, a⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
        b.snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a ≤ b
have mpr : ∀ (j : ι) (b : α j),
  (∃ (h :
      (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
        (mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
        (mk (β := fun (i : ι) ↦ α i) j b).snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨j, b⟩ := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)
have mp : a < b →
  ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i)) h <
      b.snd (β := fun (i : ι) ↦ α i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
a b : (i : ι) × α i
mp :
  a < b →
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)
⊢ a < b ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)
have mpr : (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i)) h <
      b.snd (β := fun (i : ι) ↦ α i)) →
  a < b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)) →
    a < b
have mpr : ∀ (i : ι) (a : α i),
  (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
        b.snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a < b
Tactic: obtain ⟨i, a⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
        b.snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a < b
have mpr : ∀ (j : ι) (b : α j),
  (∃ (h :
      (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
        (mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
        (mk (β := fun (i : ι) ↦ α i) j b).snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨j, b⟩ := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x x_1 : (i : ι) × α i
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x
have mp : x < x_1 → x ≤ x_1 ∧ ¬x_1 ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x x_1 : (i : ι) × α i
mp : x < x_1 → x ≤ x_1 ∧ ¬x_1 ≤ x
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x
have mpr : x ≤ x_1 ∧ ¬x_1 ≤ x → x < x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∧
    ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
have mp : a ≤ b ∧ ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
Tactic: rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
mp : a ≤ b ∧ ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∧
    ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
have mp₁ : a ≤ b ∧ ¬b ≤ a
Tactic: rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
h : ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b
have h₁ : ¬b ≤ a
Tactic: rw [mk_le_mk_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (a_1 : (i : ι) × α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
have obtain : ∀ (c : α i) (ha : a < c) (hb : c < b),
  ∃ (a_1 : (i : ι) × α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
⊢ ∀ (a b : Σₗ (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_1 : ∀ (a b : Σₗ (i : ι), α i) (hab : a < b), ¬b ≤ a
Tactic: refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
refine_1 : ∀ (a b : Σₗ (i : ι), α i) (hab : a < b), ¬b ≤ a
⊢ ∀ (a b : Σₗ (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_2 : ∀ (a b : Σₗ (i : ι), α i), a ≤ b ∧ ¬b ≤ a → a < b
Tactic: refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i j : ι
b : α i
a : α j
hji : i < j
hab : mk (β := fun (i : ι) ↦ α i) j a < mk (β := fun (i : ι) ↦ α i) i b
⊢ False
have refine_1 : ∀ (hij : j < i), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i j : ι
b : α i
a : α j
hji : i < j
hab : mk (β := fun (i : ι) ↦ α i) j a < mk (β := fun (i : ι) ↦ α i) i b
refine_1 : ∀ (hij : j < i), False
⊢ False
have refine_1₁ : ∀ (a : α i) (hji : i < i) (hab : a < b), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
Cleared hypotheses: j, a, hji, hab
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hba : b ≤ a
hab : mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b
⊢ False
have refine_1 : ∀ (hij : i < i), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hba : b ≤ a
hab : mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b
refine_1 : ∀ (hij : i < i), False
⊢ False
have refine_1₁ : ∀ (hab : a < b), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ (i : ι), α i
a : ι
b : α a
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b
have inl : ∀ (b : α ⊥), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) ⊥ b
Tactic: obtain rfl | ha := eq_bot_or_bot_lt a
Cleared hypotheses: a, b