awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Interval
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
⊢ #(Icc f g) = ∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))

Tactic:
card_dfinsupp _ _

Premises used: Finset.card_dfinsupp, Finset.map, Finset.Icc, Finset.dfinsupp
-- Module: Mathlib.Data.DFinsupp.Interval
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
rw₁ 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
⊢ #(Ico f g) =
    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]

Premises used: Finset.card_Ico_eq_card_Icc_sub_one, DFinsupp.card_Icc
-- Module: Mathlib.Data.DFinsupp.Interval
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
rw₁ 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
⊢ #(Ioc f g) =
    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]

Premises used: Finset.card_Ioc_eq_card_Icc_sub_one, DFinsupp.card_Icc
-- Module: Mathlib.Data.DFinsupp.Interval
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
rw₁ 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
⊢ #(Ioo f g) =
    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]

Premises used: Finset.card_Ioo_eq_card_Icc_sub_two, DFinsupp.card_Icc
-- Module: Mathlib.Data.DFinsupp.Interval
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
rw :
  #(uIcc f g) =
    ∏ i ∈ (f ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α), #(uIcc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))
⊢ #(uIcc f g) = ∏ i ∈ f.support (β := α) ∪ g.support (β := α), #(uIcc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))

Tactic:
rw [← support_inf_union_support_sup]

Premises used: DFinsupp.support_inf_union_support_sup
-- Module: Mathlib.Data.DFinsupp.Interval
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 ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α), #(uIcc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))

Tactic:
card_Icc _ _

Premises used: DFinsupp.card_Icc, Finset.uIcc
-- Module: Mathlib.Data.DFinsupp.Interval
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 ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α), #(uIcc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i))

Tactic:
exact card_Icc _ _

Premises used: DFinsupp.card_Icc
-- Module: Mathlib.Data.DFinsupp.Interval
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
⊢ #(Iic f) = ∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))

Tactic:
simp [Iic_eq_Icc, card_Icc, bot_eq_zero]

Premises used: Finset.Iic_eq_Icc, bot_eq_zero, DFinsupp.card_Icc
-- Module: Mathlib.Data.DFinsupp.Interval
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
rw₁ rw₂ :
  HSub.hSub (α := ℕ) (∏ i ∈ f.support (β := α), #(Iic ((f : (a : ι) → α a) i))) 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

Tactic:
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

Premises used: Finset.card_Iio_eq_card_Iic_sub_one, DFinsupp.card_Iic
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : Π₀ (i : ι), α i
⊢ Pi.Lex (β := fun {i : ι} ↦ α i) r (fun {i : ι} ↦ s i) (⇑a : (a : ι) → α a) (⇑b : (a : ι) → α a) =
    DFinsupp.Lex (α := α) r s a b

Tactic:
rfl

Premises used: DFinsupp.Lex, rfl
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : Π₀ (i : ι), α i
⊢ DFinsupp.Lex (α := α) r s a b ↔
    ∃ (j : ι),
      (∀ (d : ι), r d j → (a : (a : ι) → α a) d = (b : (a : ι) → α a) d) ∧
        s j ((a : (a : ι) → α a) j) ((b : (a : ι) → α a) j)

Tactic:
.rfl

Premises used: Iff.rfl, Pi.Lex, DFinsupp.Lex
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LT ι
inst_2 : (i : ι) → LT (α i)
a b : Lex (Π₀ (i : ι), α i)
⊢ a < b ↔
    ∃ (i : ι),
      (∀ j < i,
          (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) a : Π₀ (i : ι), α i) : (a : ι) → α a) j =
            (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) b : Π₀ (i : ι), α i) : (a : ι) → α a) j) ∧
        (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) a : Π₀ (i : ι), α i) : (a : ι) → α a) i <
          (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) b : Π₀ (i : ι), α i) : (a : ι) → α a) i

Tactic:
.rfl

Premises used: Iff.rfl, Pi.Lex, DFinsupp.Lex
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LT ι
inst_2 : (i : ι) → LT (α i)
a b : Colex (Π₀ (i : ι), α i)
⊢ a < b ↔
    ∃ (i : ι),
      (∀ (j : ι),
          i < j →
            (((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) a : Π₀ (i : ι), α i) : (a : ι) → α a) j =
              (((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) b : Π₀ (i : ι), α i) : (a : ι) → α a) j) ∧
        (((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) a : Π₀ (i : ι), α i) : (a : ι) → α a) i <
          (((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) b : Π₀ (i : ι), α i) : (a : ι) → α a) i

Tactic:
.rfl

Premises used: Iff.rfl, Pi.Lex, DFinsupp.Lex
-- Module: Mathlib.Data.DFinsupp.Lex
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
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
⊢ ∃ (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

Premises used: Pi.lt_def, Iff.mp
-- Module: Mathlib.Data.DFinsupp.Lex
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
⊢ (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r

Tactic:
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
-- Module: Mathlib.Data.DFinsupp.Lex
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
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
⊢ ∃ (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⟩

Premises used: Iff.mpr, DFinsupp.mem_neLocus, setOf, Subtype.mk, LT.lt, Exists.intro, WellFounded.has_min, Subtype.val, DFunLike.coe, LT.lt.ne
-- Module: Mathlib.Data.DFinsupp.Lex
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

Tactic:
⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩

Premises used: And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Data.DFinsupp.Lex
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
refine : ∀ (k : ι) (hk : r k (↑i : ι)), (y : (a : ι) → α a) k ≤ (x : (a : ι) → α a) k
⊢ ∃ (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:
refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩
-- Module: Mathlib.Data.DFinsupp.Lex
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
k : ι
hk : r k (↑i : ι)
⊢ (y : (a : ι) → α a) k ≤ (x : (a : ι) → α a) k

Tactic:
of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_ge h) hk

Premises used: Iff.mpr, LE.le.lt_of_not_ge, DFinsupp.mem_neLocus, Ne.symm, Subtype.mk, of_not_not, ne_of_not_le
-- Module: Mathlib.Data.DFinsupp.Lex
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
k : ι
hk : r k (↑i : ι)
⊢ (y : (a : ι) → α a) k ≤ (x : (a : ι) → α a) k

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

Premises used: Iff.mpr, LE.le.lt_of_not_ge, DFinsupp.mem_neLocus, Ne.symm, Subtype.mk, of_not_not, ne_of_not_le
-- Module: Mathlib.Data.DFinsupp.Lex
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
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
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)
    (k : ι) (hk : r k (↑i : ι)), (y : (a : ι) → α a) k ≤ (x : (a : ι) → α a) k
⊢ ∃ (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
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
simp_rw :
  ∃ (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
⊢ Pi.Lex (β := α) r (fun {i : ι} (x1 x2 : α i) ↦ x1 < x2) (⇑x : (a : ι) → α a) (⇑y : (a : ι) → α a)

Tactic:
simp_rw [Pi.Lex, le_antisymm_iff]

Premises used: Pi.Lex, le_antisymm_iff
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α 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

Tactic:
lex_lt_of_lt_of_preorder r hlt

Premises used: DFinsupp.lex_lt_of_lt_of_preorder
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α 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

Tactic:
exact lex_lt_of_lt_of_preorder r hlt

Premises used: DFinsupp.lex_lt_of_lt_of_preorder
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : Unique ι
inst_2 : (i : ι) → LT (α i)
r : ι → ι → Prop
inst_3 : Std.Irrefl r
x y : Π₀ (i : ι), α i
⊢ DFinsupp.Lex (α := α) r (fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) x y ↔
    LT.lt (α := α default) ((x : (a : ι) → α a) default) ((y : (a : ι) → α a) default)

Tactic:
Pi.lex_iff_of_unique

Premises used: Pi.lex_iff_of_unique, DFinsupp.Lex
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : Unique ι
inst_2 : (i : ι) → LT (α i)
inst_3 : Preorder ι
x y : Lex (Π₀ (i : ι), α i)
⊢ x < y ↔
    LT.lt (α := α default)
      ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) default)
      ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) y : Π₀ (i : ι), α i) : (a : ι) → α a) default)

Tactic:
lex_iff_of_unique

Premises used: DFinsupp.lex_iff_of_unique
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : Unique ι
inst_2 : (i : ι) → LT (α i)
inst_3 : Preorder ι
x y : Colex (Π₀ (i : ι), α i)
⊢ x < y ↔
    LT.lt (α := α default)
      ((((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) default)
      ((((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) y : Π₀ (i : ι), α i) : (a : ι) → α a) default)

Tactic:
lex_iff_of_unique

Premises used: DFinsupp.lex_iff_of_unique
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
⊢ IsStrictOrder (Colex (Π₀ (i : ι), α i)) fun (x1 x2 : Colex (Π₀ (i : ι), α i)) ↦ x1 < x2

Tactic:
Lex.isStrictOrder (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.isStrictOrder, OrderDual