awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Cover
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
h₂ : ¬c j < b j
⊢ (fun (x1 x2 : α j) ↦ x1 ≤ x2) (b j) (a j)

Tactic:
simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Cover
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
h₂ : ¬c j < b j
⊢ AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩
-- Module: Mathlib.Order.Cover
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)
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)
⊢ ∃ (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₂⟩

Premises used: and_imp, Pi.lt_def, CovBy, forall_exists_index, not_exists, not_and
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
⊢ a ⋖ b ∨ a ≤ b ∧ b ≤ a

Tactic:
rw [wcovBy_iff_covBy_or_le_and_le] at h

Premises used: wcovBy_iff_covBy_or_le_and_le
-- Module: Mathlib.Order.Cover
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)
inr : ∀ (h : a ≤ b ∧ b ≤ a), ∃ (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)

Tactic:
obtain h | h := h
-- Module: Mathlib.Order.Cover
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)

Tactic:
exists_forall_antisymmRel_of_covBy h

Premises used: Pi.exists_forall_antisymmRel_of_covBy
-- Module: Mathlib.Order.Cover
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)

Tactic:
exact exists_forall_antisymmRel_of_covBy h

Premises used: Pi.exists_forall_antisymmRel_of_covBy
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ≤ b ∧ b ≤ a
inr : ∀ (inhabited_h : Inhabited ι), ∃ (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)

Tactic:
inhabit ι
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ≤ b ∧ b ≤ a
inhabited_h : Inhabited ι
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
⟨default, fun j hj ↦ ⟨h.left j, h.right j⟩⟩

Premises used: Inhabited.default, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ≤ b ∧ b ≤ a
inhabited_h : Inhabited ι
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
exact ⟨default, fun j hj ↦ ⟨h.left j, h.right j⟩⟩
-- Module: Mathlib.Order.Cover
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)
mpr : (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)) → a ⩿ b
⊢ a ⩿ b ↔ ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
constructor
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
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)
⊢ ∃ (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

Premises used: Pi.exists_forall_antisymmRel_of_wcovBy
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
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:
⟨i, h.eval _, hi⟩

Premises used: WCovBy.eval, And.intro, Exists.intro
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
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:
exact ⟨i, h.eval _, hi⟩
-- Module: Mathlib.Order.Cover
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

Tactic:
⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hab.1) (h j · |>.1), fun c hac hcb ↦ ?_⟩

Premises used: Eq.rec, And.left, And.intro, WCovBy, eq_or_ne, Or.elim, Eq.symm
-- Module: Mathlib.Order.Cover
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)
mpr : ∀ (c : (i : ι) → α i) (hac : a < c) (hcb : c < b), False
⊢ a ⩿ b

Tactic:
refine ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hab.1) (h j · |>.1), fun c hac hcb ↦ ?_⟩
-- Module: Mathlib.Order.Cover
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
obtain : ∀ (hac : a ≤ c) (j : ι) (hj : a j < c j), a i < c i
⊢ a i < c i

Tactic:
obtain ⟨hac, j, hj⟩ := Pi.lt_def.1 hac

Premises used: Pi.lt_def, Iff.mp
-- Module: Mathlib.Order.Cover
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_1 : a < c
hcb : c < b
hac : a ≤ c
j : ι
hj : a j < c j
⊢ a i < c i

Tactic:
(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

Premises used: False.elim, Eq.rec, LT.lt.le, lt_of_antisymmRel_of_lt, eq_or_ne, LT.lt.not_ge, Or.elim, AntisymmRel.symm
-- Module: Mathlib.Order.Cover
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_1 : a < c
hcb : c < b
hac : a ≤ c
j : ι
hj : a j < c j
⊢ a i < c i

Tactic:
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

Premises used: False.elim, LT.lt.le, lt_of_antisymmRel_of_lt, eq_or_ne, LT.lt.not_ge, Or.elim, AntisymmRel.symm
-- Module: Mathlib.Order.Cover
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

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
-- Module: Mathlib.Order.Cover
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
obtain : ∀ (hcb : c ≤ b) (j : ι) (hj : c j < b j), c i < b i
⊢ c i < b i

Tactic:
obtain ⟨hcb, j, hj⟩ := Pi.lt_def.1 hcb

Premises used: Pi.lt_def, Iff.mp
-- Module: Mathlib.Order.Cover
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_1 : c < b
haci : a i < c i
hcb : c ≤ b
j : ι
hj : c j < b j
⊢ c i < b i

Tactic:
(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

Premises used: False.elim, Eq.rec, LT.lt.le, eq_or_ne, LT.lt.not_ge, Or.elim, AntisymmRel.symm, lt_of_lt_of_antisymmRel
-- Module: Mathlib.Order.Cover
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_1 : c < b
haci : a i < c i
hcb : c ≤ b
j : ι
hj : c j < b j
⊢ c i < b i

Tactic:
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

Premises used: False.elim, LT.lt.le, eq_or_ne, LT.lt.not_ge, Or.elim, AntisymmRel.symm, lt_of_lt_of_antisymmRel
-- Module: Mathlib.Order.Cover
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

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
-- Module: Mathlib.Order.Cover
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
hcbi : c i < b i
⊢ False

Tactic:
hab.2 haci hcbi

Premises used: And.right
-- Module: Mathlib.Order.Cover
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
hcbi : c i < b i
⊢ False

Tactic:
exact hab.2 haci hcbi

Premises used: And.right
-- Module: Mathlib.Order.Cover
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)
mpr : (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)) → a ⋖ b
⊢ a ⋖ b ↔ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
constructor
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
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)
⊢ ∃ (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

Premises used: Pi.lt_def, And.right, And.left, Iff.mp
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨j⟩
-- Module: Mathlib.Order.Cover
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 ι
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)
⊢ ∃ (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

Premises used: Pi.exists_forall_antisymmRel_of_wcovBy, CovBy.wcovBy
-- Module: Mathlib.Order.Cover
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 = j

Tactic:
by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj

Premises used: Ne.symm, And.right, LE.le.not_gt, by_contra
-- Module: Mathlib.Order.Cover
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)
⊢ a i < b i

Tactic:
obtain rfl : i = j := by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj

Premises used: Ne.symm, And.right, LE.le.not_gt, by_contra, rfl
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
this : Nonempty ι
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
hj : a i < b i
⊢ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
⟨i, covBy_iff_wcovBy_and_lt.2 ⟨h.wcovBy.eval i, hj⟩, hi⟩

Premises used: Iff.mpr, WCovBy.eval, And.intro, Exists.intro, CovBy.wcovBy, covBy_iff_wcovBy_and_lt
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
this : Nonempty ι
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
hj : a i < b i
⊢ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
exact ⟨i, covBy_iff_wcovBy_and_lt.2 ⟨h.wcovBy.eval i, hj⟩, hi⟩
-- Module: Mathlib.Order.Cover
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)
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨i⟩
-- Module: Mathlib.Order.Cover
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

Tactic:
covBy_iff_wcovBy_and_lt.2 ⟨wcovBy_iff_antisymmRel.2 ⟨i, hi.wcovBy, h⟩, ?_⟩

Premises used: Iff.mpr, Pi.wcovBy_iff_antisymmRel, And.intro, Exists.intro, CovBy.wcovBy, covBy_iff_wcovBy_and_lt
-- Module: Mathlib.Order.Cover
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 ι
mpr : a < b
⊢ a ⋖ b

Tactic:
refine covBy_iff_wcovBy_and_lt.2 ⟨wcovBy_iff_antisymmRel.2 ⟨i, hi.wcovBy, h⟩, ?_⟩

Premises used: Iff.mpr, Pi.wcovBy_iff_antisymmRel, And.intro, Exists.intro, CovBy.wcovBy, covBy_iff_wcovBy_and_lt
-- Module: Mathlib.Order.Cover
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

Tactic:
Pi.lt_def.2 ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hi.1.le) (h j · |>.1), i, hi.1⟩

Premises used: Iff.mpr, Pi.lt_def, Eq.rec, LT.lt.le, And.left, And.intro, Exists.intro, eq_or_ne, Or.elim, Eq.symm
-- Module: Mathlib.Order.Cover
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

Tactic:
exact Pi.lt_def.2 ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hi.1.le) (h j · |>.1), i, hi.1⟩

Premises used: Iff.mpr, Pi.lt_def, And.left, And.intro, Exists.intro, eq_or_ne, Or.elim
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
h : a ⋖ b
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
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j

Tactic:
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_covBy h

Premises used: Pi.exists_forall_antisymmRel_of_covBy
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
h : a ⋖ b
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:
⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

Premises used: AntisymmRel.eq, Exists.intro
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
h : a ⋖ b
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:
exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
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
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j

Tactic:
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h

Premises used: Pi.exists_forall_antisymmRel_of_wcovBy
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
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:
⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

Premises used: AntisymmRel.eq, Exists.intro
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
h : a ⩿ b
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:
exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
⊢ a ⩿ b ↔ ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
simp [wcovBy_iff_antisymmRel]

Premises used: Pi.wcovBy_iff_antisymmRel
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
⊢ a ⋖ b ↔ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
simp [covBy_iff_antisymmRel]

Premises used: Pi.covBy_iff_antisymmRel
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
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
⊢ a ⩿ b ↔ ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x

Tactic:
rw [wcovBy_iff]

Premises used: Pi.wcovBy_iff
-- Module: Mathlib.Order.Cover
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
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
⊢ (∃ (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
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ b = Function.update (β := α) a i (b i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

Premises used: eq_comm, Function.eq_update_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update (β := α) a i x

Tactic:
exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
x : α i
h : a i ⩿ x
⊢ a i ⩿ Function.update (β := α) a i x i ∧ ∀ (j : ι), j ≠ i → a j = Function.update (β := α) a i x j

Tactic:
simpa +contextual
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
x : α i
h : a i ⩿ x
⊢ ∃ (i_1 : ι), a i_1 ⩿ Function.update (β := α) a i x i_1 ∧ ∀ (j : ι), j ≠ i_1 → a j = Function.update (β := α) a i x j

Tactic:
exact ⟨i, by simpa +contextual⟩