awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
⊢ #(Ico f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
have rw : #(Icc f g) - 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
rw :
  #(Icc f g) - 1 =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
⊢ #(Ico f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
have rw₁ : HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
⊢ #(Ioc f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
have rw : #(Icc f g) - 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
rw :
  #(Icc f g) - 1 =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
⊢ #(Ioc f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
have rw₁ : HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
⊢ #(Ioo f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 2
have rw : #(Icc f g) - 2 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
rw :
  #(Icc f g) - 2 =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 2
⊢ #(Ioo f g) =
    HSub.hSub (α := ℕ)
      (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 2
have rw₁ : HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 2 =
  HSub.hSub (α := ℕ)
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)) 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Lattice α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) =
    ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (uIcc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
have rw : #(uIcc f g) =
  ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support,
    card.{u_2} (α := α) (uIcc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
Tactic: rw [← support_inf_union_support_sup]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsBotZeroClass α
inst_3 : OrderBot α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq ι
inst_6 : DecidableEq α
f : ι →₀ α
⊢ #(Iio f) = HSub.hSub (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)) 1
have rw : #(Iic f) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)) 1
Tactic: rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsBotZeroClass α
inst_3 : OrderBot α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq ι
inst_6 : DecidableEq α
f : ι →₀ α
rw : #(Iic f) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)) 1
⊢ #(Iio f) = HSub.hSub (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)) 1 =
  HSub.hSub (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)) 1
Tactic: rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
⊢ WellFounded (Finsupp.DegLex r s)
have wft : WellFounded (α := ℕ × (α →₀ ℕ)) (Prod.Lex s (Finsupp.Lex r s))
Tactic: have wft := WellFounded.prod_lex hs (Finsupp.Lex.wellFounded' hs0 hs hr)
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : WellFounded (α := ℕ × (α →₀ ℕ)) (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Finsupp.DegLex r s)
have wft₁ : Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) Set.univ (Prod.Lex s (Finsupp.Lex r s))
Tactic: rw [← Set.wellFoundedOn_univ] at wft
Cleared hypotheses: wft
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) Set.univ (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (α := α →₀ ℕ)
    (Function.onFun (β := ℕ × (α →₀ ℕ)) (Prod.Lex s (Finsupp.Lex r s)) fun (x : α →₀ ℕ) ↦
      ((degree : (a : α →₀ ℕ) → ℕ) x, x))
have rw : Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) (Set.range fun (x : α →₀ ℕ) ↦ ((degree : (a : α →₀ ℕ) → ℕ) x, x))
  (Prod.Lex s (Finsupp.Lex r s))
Tactic: rw [← Set.wellFoundedOn_range]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : a < b
hbc : b < c
⊢ a < c
have simp : ∀
  (hab :
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∧
        LT.lt (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) :
            Lex (α →₀ ℕ)))
  (hbc :
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
        LT.lt (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) :
            Lex (α →₀ ℕ))),
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: simp only [lt_iff] at hab hbc ⊢
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
hbc :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
⊢ LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
have inl : ∀
  (hab :
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)),
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: rcases hab with (hab | hab)
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hbc :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
⊢ LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
have inl : ∀
  (hbc :
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)),
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: rcases hbc with (hbc | hbc)
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
hbc :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)
⊢ LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
have inl : LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
  ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
hbc :
  Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
    LT.lt (α := Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
⊢ LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
have inl : LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
  ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hbc :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
hab :
  Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∧
    LT.lt (α := Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
⊢ LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
have inr : ∀
  (hbc :
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)),
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: rcases hbc with (hbc | hbc)
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∧
    LT.lt (α := Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
hbc :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)
⊢ LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
have inr : LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
  ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)
Tactic: left