awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst_2 : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support (β := fun (i : ι) ↦ Finset (α i)) ⊆ s
i : ι
h : (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
hi : i ∈ f.support (β := α)
H : (t : (a : ι) → Finset (α a)) i = 0
refine_2 :
  ∀ (h : Membership.mem (γ := Finset (α i)) 0 ((f : (a : ι) → α a) i)) (hi : i ∈ f.support (β := α))
    (H : (t : (a : ι) → Finset (α a)) i = 0), (f : (a : ι) → α a) i = 0
⊢ (f : (a : ι) → α a) i = 0
have refine_2₁ : ∀ (h : (f : (a : ι) → α a) i = 0) (hi : i ∈ f.support (β := α)) (H : (t : (a : ι) → Finset (α a)) i = 0),
  (f : (a : ι) → α a) i = 0
Tactic: rwa [H, mem_zero] at h
Cleared hypotheses: h, hi, H
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
f_1 g_1 : Π₀ (i : ι), α i
i_1 : ι
a : α i_1
f g : Π₀ (i : ι), α i
fs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ α i) i = 0 }
gs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g.toFun (β := fun (i : ι) ↦ α i) i = 0 }
i : ι
h : i ∉ (↑fs : Multiset ι) + (↑gs : Multiset ι)
⊢ Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i) = 0
have hf : (f : (a : ι) → α a) i = 0
Tactic: have hf : f i = 0 := (fs.prop i).resolve_left
            (Multiset.notMem_mono (Multiset.Le.subset <| Multiset.le_add_right _ _) h)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
f_1 g_1 : Π₀ (i : ι), α i
i_1 : ι
a : α i_1
f g : Π₀ (i : ι), α i
fs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ α i) i = 0 }
gs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g.toFun (β := fun (i : ι) ↦ α i) i = 0 }
i : ι
h : i ∉ (↑fs : Multiset ι) + (↑gs : Multiset ι)
hf : (f : (a : ι) → α a) i = 0
⊢ Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i) = 0
have hg : (g : (a : ι) → α a) i = 0
Tactic: have hg : g i = 0 := (gs.prop i).resolve_left
            (Multiset.notMem_mono (Multiset.Le.subset <| Multiset.le_add_left _ _) h)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
f_1 g_1 : Π₀ (i : ι), α i
i_1 : ι
a : α i_1
f g : Π₀ (i : ι), α i
fs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ α i) i = 0 }
gs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g.toFun (β := fun (i : ι) ↦ α i) i = 0 }
i : ι
h : i ∉ (↑fs : Multiset ι) + (↑gs : Multiset ι)
hf : (f : (a : ι) → α a) i = 0
hg : (g : (a : ι) → α a) i = 0
⊢ Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i) = 0
have simp_rw : Eq.{u_2 + 1} (α := Finset (α i)) (Icc 0 0) 0
Tactic: simp_rw [hf, hg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (α i)
⊢ (f.rangeIcc (α := α) g).support (β := fun (i : ι) ↦ Finset (α i)) ⊆ f.support (β := α) ∪ g.support (β := α)
have refine : ∀ (x : ι) (hx : x ∈ (f.rangeIcc (α := α) g).support (β := fun (i : ι) ↦ Finset (α i))),
  x ∈ f.support (β := α) ∪ g.support (β := α)
Tactic: refine fun x hx => ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc (α := α) g).support (β := fun (i : ι) ↦ Finset (α i))
⊢ x ∈ f.support (β := α) ∪ g.support (β := α)
have by_contra : ∀ (h : x ∉ f.support (β := α) ∪ g.support (β := α)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc (α := α) g).support (β := fun (i : ι) ↦ Finset (α i))
h : x ∉ f.support (β := α) ∪ g.support (β := α)
⊢ False
have refine : (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) x = 0
Tactic: refine notMem_support_iff.2 ?_ hx
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc (α := α) g).support (β := fun (i : ι) ↦ Finset (α i))
h : x ∉ f.support (β := α) ∪ g.support (β := α)
⊢ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) x = 0
have rw : Eq.{u_2 + 1} (α := Finset (α x)) (Icc 0 0) 0
Tactic: rw [rangeIcc_apply, notMem_support_iff.1 (notMem_mono subset_union_left h),
    notMem_support_iff.1 (notMem_mono subset_union_right h)]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ #(f.pi (α := α)) =
    f.prod (β := fun (i : ι) ↦ Finset (α i)) fun (i : ι) ↦ (↑(#((f : (a : ι) → Finset (α a)) i)) : Finset (α i) → ℕ)
have rw : Eq (α := ℕ) (∏ i ∈ f.support (β := fun (i : ι) ↦ Finset (α i)), #((f : (a : ι) → Finset (α a)) i))
  (f.prod (β := fun (i : ι) ↦ Finset (α i)) fun (i : ι) ↦ (↑(#((f : (a : ι) → Finset (α a)) i)) : Finset (α i) → ℕ))
Tactic: rw [pi, card_dfinsupp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i))
      ((fun (f g : Π₀ (i : ι), α i) ↦
          ((f.support (β := α) ∪ g.support (β := α)).dfinsupp (α := α)
              (⇑(f.rangeIcc (α := α) g) : (a : ι) → Finset (α a)) :
            Finset (Π₀ (i : ι), α i)))
        f g)
      x ↔
    f ≤ x ∧ x ≤ g
have refine : (∀ (i : ι), (x : (a : ι) → α a) i ∈ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) i) ↔ f ≤ x ∧ x ≤ g
Tactic: refine (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), (x : (a : ι) → α a) i ∈ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) i) ↔ f ≤ x ∧ x ≤ g
have simp_rw : ((∀ (x_1 : ι), (f : (a : ι) → α a) x_1 ≤ (x : (a : ι) → α a) x_1) ∧
    ∀ (x_1 : ι), (x : (a : ι) → α a) x_1 ≤ (g : (a : ι) → α a) x_1) ↔
  f ≤ x ∧ x ≤ g
Tactic: simp_rw [mem_rangeIcc_apply_iff, forall_and]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ico f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
have rw : #(Icc f g) - 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
rw :
  #(Icc f g) - 1 =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
⊢ #(Ico f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
have rw₁ : HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioc f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
have rw : #(Icc f g) - 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
rw :
  #(Icc f g) - 1 =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
⊢ #(Ioc f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
have rw₁ : HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioo f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 2
have rw : #(Icc f g) - 2 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
rw :
  #(Icc f g) - 2 =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 2
⊢ #(Ioo f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 2
have rw₁ : HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 2 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))) 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → Lattice (α i)
inst_3 : (i : ι) → Zero (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(uIcc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))
have rw : #(uIcc f g) =
  ∏ i ∈ (f ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α), #(uIcc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))
Tactic: rw [← support_inf_union_support_sup]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → AddCommMonoid (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_5 : (i : ι) → OrderBot (α i)
inst_6 : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iio f) = HSub.hSub (α := ℕ) (∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))) 1
have rw : #(Iic f) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))) 1
Tactic: rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → AddCommMonoid (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_5 : (i : ι) → OrderBot (α i)
inst_6 : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
rw : #(Iic f) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))) 1
⊢ #(Iio f) = HSub.hSub (α := ℕ) (∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))) 1 =
  HSub.hSub (α := ℕ) (∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))) 1
Tactic: rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have obtain : ∀ (hle : (⇑x : (a : ι) → α a) ≤ (⇑y : (a : ι) → α a)) (j : ι) (hlt : (x : (a : ι) → α a) j < (y : (a : ι) → α a) j),
  ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
Tactic: obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt_1 : x < y
hle : (⇑x : (a : ι) → α a) ≤ (⇑y : (a : ι) → α a)
j : ι
hlt : (x : (a : ι) → α a) j < (y : (a : ι) → α a) j
⊢ ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r
Tactic: have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt_1 : x < y
hle : (⇑x : (a : ι) → α a) ≤ (⇑y : (a : ι) → α a)
j : ι
hlt : (x : (a : ι) → α a) j < (y : (a : ι) → α a) j
this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r
⊢ ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have obtain : ∀ (i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
  (hi :
    Membership.mem (γ := Set { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
      {i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
        LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
      i)
  (hl :
    ∀ (x_1 : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) }),
      Membership.mem (γ := Set { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
          {i : { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
            LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
          x_1 →
        ¬Subrel r (fun (x_2 : ι) ↦ x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι)) x_1 i),
  ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
Tactic: obtain ⟨i, hi, hl⟩ := this.has_min { i | x i < y i } ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt_1 : x < y
hle : (⇑x : (a : ι) → α a) ≤ (⇑y : (a : ι) → α a)
j : ι
hlt : (x : (a : ι) → α a) j < (y : (a : ι) → α a) j
this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r
i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) }
hi :
  Membership.mem (γ := Set { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
    {i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
      LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
    i
hl :
  ∀ (x_1 : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) }),
    Membership.mem (γ := Set { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
        {i : { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
          LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
        x_1 →
      ¬Subrel r (fun (x_2 : ι) ↦ x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι)) x_1 i
⊢ ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have refine : ∀ (k : ι) (hk : r k (↑i : ι)), (y : (a : ι) → α a) k ≤ (x : (a : ι) → α a) k
Tactic: refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt_1 : x < y
hle : (⇑x : (a : ι) → α a) ≤ (⇑y : (a : ι) → α a)
j : ι
hlt : (x : (a : ι) → α a) j < (y : (a : ι) → α a) j
⊢ ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have have : ∀ (this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r),
  ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
Tactic: classical
  have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
  obtain ⟨i, hi, hl⟩ := this.has_min { i | x i < y i } ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
  refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩
  exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_ge h) hk
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt_1 : x < y
hle : (⇑x : (a : ι) → α a) ≤ (⇑y : (a : ι) → α a)
j : ι
hlt : (x : (a : ι) → α a) j < (y : (a : ι) → α a) j
have have₁ have₂ :
  ∀ (this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r),
    ∃ (i : ι),
      (∀ (j : ι),
          r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
        (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
⊢ ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have have₃ : ∀ (this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r)
  (i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
  (hi :
    Membership.mem (γ := Set { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
      {i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
        LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
      i)
  (hl :
    ∀ (x_1 : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) }),
      Membership.mem (γ := Set { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
          {i : { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
            LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
          x_1 →
        ¬Subrel r (fun (x_2 : ι) ↦ x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι)) x_1 i),
  ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
Tactic: classical
  have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
  obtain ⟨i, hi, hl⟩ := this.has_min { i | x i < y i } ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
  refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩
  exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_ge h) hk