awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have h₁ : (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧ ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
Tactic: simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h :
  (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
    ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have obtain : ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
  (hi : a i < b i), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have refine : ∀ (j : ι) (hj : j ≠ i), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: refine ⟨i, fun j hj ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update (β := α) a i (b i)
⊢ AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have h₁ : c ≤ b
Tactic: have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update (β := α) a i (b i)
h₁ : c ≤ b
⊢ AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have h₂ : ¬c j < b j
Tactic: have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have simp : ∀
  (h :
    (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
      ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x),
  ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: classical
  simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
simp :
  ∀
    (h :
      (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
        ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x),
    ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have simp₁ : ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
  (hi : a i < b i), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: classical
  simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
simp :
  ∀
    (h :
      (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
        ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x),
    ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₁ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have simp₂ : ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
  (hi : a i < b i) (j : ι) (hj : j ≠ i), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: classical
  simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
simp :
  ∀
    (h :
      (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
        ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x),
    ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₁ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₂ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i) (j : ι) (hj : j ≠ i), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₃ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i) (j : ι) (hj : j ≠ i), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have simp₄ : ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
  (hi : a i < b i) (j : ι) (hj : j ≠ i),
  let c := Function.update (β := α) a i (b i);
  ∀ (h₁ : c ≤ b), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: classical
  simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
simp :
  ∀
    (h :
      (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
        ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x),
    ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₁ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₂ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i) (j : ι) (hj : j ≠ i), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₃ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i) (j : ι) (hj : j ≠ i), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
simp₄ :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i) (j : ι) (hj : j ≠ i),
    let c := Function.update (β := α) a i (b i);
    ∀ (h₁ : c ≤ b), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have simp₅ : ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
  (hi : a i < b i) (j : ι) (hj : j ≠ i),
  let c := Function.update (β := α) a i (b i);
  ∀ (h₁ : c ≤ b) (h₂ : ¬c j < b j), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: classical
  simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have h₁ : a ⋖ b ∨ a ≤ b ∧ b ≤ a
Tactic: rw [wcovBy_iff_covBy_or_le_and_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⋖ b ∨ a ≤ b ∧ b ≤ a
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have inl : ∀ (h : a ⋖ b), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⋖ b ∨ a ≤ b ∧ b ≤ a
inl : ∀ (h : a ⋖ b), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have inr : ∀ (h : a ≤ b ∧ b ≤ a), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ≤ b ∧ b ≤ a
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have inr : ∀ (inhabited_h : Inhabited ι), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
⊢ a ⩿ b ↔ ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have mp : a ⩿ b → ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
mp : a ⩿ b → ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ a ⩿ b ↔ ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have mpr : (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)) → a ⩿ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
⊢ ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have mp : ∀ (i : ι) (hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)),
  ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ a ⩿ b
have mpr : ∀ (c : (i : ι) → α i) (hac : a < c) (hcb : c < b), False
Tactic: refine ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hab.1) (h j · |>.1), fun c hac hcb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
⊢ a i < c i
have obtain : ∀ (hac : a ≤ c) (j : ι) (hj : a j < c j), a i < c i
Tactic: obtain ⟨hac, j, hj⟩ := Pi.lt_def.1 hac
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
⊢ False
have haci : a i < c i
Tactic: have haci : a i < c i := by
    obtain ⟨hac, j, hj⟩ := Pi.lt_def.1 hac
    exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦
      ((lt_of_antisymmRel_of_lt (h j hj').symm hj).not_ge (hcb.le j)).elim
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
haci : a i < c i
⊢ c i < b i
have obtain : ∀ (hcb : c ≤ b) (j : ι) (hj : c j < b j), c i < b i
Tactic: obtain ⟨hcb, j, hj⟩ := Pi.lt_def.1 hcb
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
haci : a i < c i
⊢ False
have hcbi : c i < b i
Tactic: have hcbi : c i < b i := by
    obtain ⟨hcb, j, hj⟩ := Pi.lt_def.1 hcb
    exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦
      ((lt_of_lt_of_antisymmRel hj (h j hj').symm).not_ge (hac.le j)).elim
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
⊢ a ⋖ b ↔ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have mp : a ⋖ b → ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
mp : a ⋖ b → ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ a ⋖ b ↔ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have mpr : (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)) → a ⋖ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have mp : ∀ (j : ι) (hj : a j < b j),
  ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: obtain ⟨j, hj⟩ := (Pi.lt_def.1 h.1).2
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
⊢ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨j⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
this : Nonempty ι
⊢ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have mp : ∀ (i : ι) (hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)),
  ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
Tactic: obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h.wcovBy
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
this : Nonempty ι
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
have hj₁ : a i < b i
Tactic: obtain rfl : i = j := by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ a ⋖ b
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨i⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
this : Nonempty ι
⊢ a ⋖ b
have mpr : a < b
Tactic: refine covBy_iff_wcovBy_and_lt.2 ⟨wcovBy_iff_antisymmRel.2 ⟨i, hi.wcovBy, h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j
have obtain : ∀ (i : ι) (hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)),
  ∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j
Tactic: obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_covBy h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j
have obtain : ∀ (i : ι) (hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)),
  ∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j
Tactic: obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
⊢ a ⩿ b ↔ ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x
have rw : (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
  ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x
Tactic: rw [wcovBy_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
⊢ (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x
have mp : (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
  ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
mp :
  (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
    ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x
⊢ (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x
have mpr : (∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x) →
  ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
⊢ a ⋖ b ↔ ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
have rw : (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
  ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
Tactic: rw [covBy_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
⊢ (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
have mp : (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
  ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
mp :
  (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
    ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
⊢ (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
have mpr : (∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x) →
  ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
⊢ a ⩿ b ↔ ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x
have rw : (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
  ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x
Tactic: rw [wcovBy_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
⊢ (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x
have mp : (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
  ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x
Tactic: constructor