awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s t : Finset ι
f : (i : ι) → i ∈ s → α
inst_1 : DecidableEq ι
⊢ Eq (α := ι →₀ α) (indicator t fun (i : ι) (x : i ∈ t) ↦ (indicator s f : (a : ι) → α) i)
    (indicator (s ∩ t) fun (i : ι) (hi : i ∈ s ∩ t) ↦ f i ⋯)

Tactic:
grind [indicator_apply]

Premises used: Finsupp.indicator_apply
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
simp : (∀ (x : ι), g x = if hi : x ∈ s then f x hi else 0) ↔ ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i

Tactic:
simp only [this, funext_iff, indicator_apply]

Premises used: funext_iff, Finsupp.indicator_apply
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ (∀ (x : ι), g x = if hi : x ∈ s then f x hi else 0) ↔ ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
suffices :
  (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i

Tactic:
suffices g.support ⊆ s ∧ (∀ i (hi : i ∈ s), f i hi = g i) ↔
      (∀ i, if hi : i ∈ s then f i hi = g i else g i = 0) by
    simp only [this, funext_iff, indicator_apply]
    grind
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
rw :
  ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0

Tactic:
rw [Set.subset_def, and_comm]

Premises used: Set.subset_def, and_comm
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
    (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ (i : ι) (hi : i ∉ s), g i = 0

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
    (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ (i : ι) (hi : i ∉ s), g i = 0

Tactic:
have : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i (hi : i ∉ s), g i = 0) := by grind
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
    (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ (i : ι) (hi : i ∉ s), g i = 0
⊢ ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0

Tactic:
simp [this, not_imp_comm]

Premises used: not_imp_comm
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
suffices suffices₁ suffices₂ :
  (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
suffices₃ :
  ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
suffices₄ :
  ∀
    (this :
      (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
        (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ (i : ι) (hi : i ∉ s), g i = 0),
    ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
      ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i

Tactic:
classical
  suffices g.support ⊆ s ∧ (∀ i (hi : i ∈ s), f i hi = g i) ↔
      (∀ i, if hi : i ∈ s then f i hi = g i else g i = 0) by
    simp only [this, funext_iff, indicator_apply]
    grind
  rw [Set.subset_def, and_comm]
  have : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i (hi : i ∉ s), g i = 0) := by grind
  simp [this, not_imp_comm]

Premises used: Set.subset_def, not_imp_comm, and_comm
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
d : ι →₀ α
⊢ (d = indicator s fun (i : ι) (x : i ∈ s) ↦ (d : (a : ι) → α) i) ↔ d.support ⊆ s

Tactic:
grind [indicator]

Premises used: Finsupp.indicator
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f_1 : ι →₀ α
i_1 : ι
a : α
f : ι →₀ α
i : ι
rw :
  Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ↔
    Eq (α := Finset α) (singleton (α := α) ((f : (a : ι) → α) i : α)) 0
⊢ i ∈ f.support ↔ Ne (α := Finset α) (singleton (α := α) ((f : (a : ι) → α) i : α)) 0

Tactic:
rw [← not_iff_not, notMem_support_iff, not_ne_iff]

Premises used: not_iff_not, Finsupp.notMem_support_iff, not_ne_iff
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f_1 : ι →₀ α
i_1 : ι
a : α
f : ι →₀ α
i : ι
⊢ Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ↔
    Eq (α := Finset α) (singleton (α := α) ((f : (a : ι) → α) i : α)) 0

Tactic:
singleton_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, Finset.singleton_injective, Iff.symm
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f_1 : ι →₀ α
i_1 : ι
a : α
f : ι →₀ α
i : ι
⊢ Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ↔
    Eq (α := Finset α) (singleton (α := α) ((f : (a : ι) → α) i : α)) 0

Tactic:
exact singleton_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, Finset.singleton_injective, Iff.symm
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f : ι →₀ α
i : ι
a : α
⊢ Membership.mem (γ := Finset α) ((f.rangeSingleton : (a : ι) → Finset α) i : Finset α) a ↔ a = (f : (a : ι) → α) i

Tactic:
mem_singleton

Premises used: Finset.mem_singleton, Set.Mem, setOf
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
f_1 g_1 : ι →₀ α
i_1 : ι
a : α
f g : ι →₀ α
i : ι
rw :
  Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ∧ Eq.{u_2 + 1} (α := α) ((g : (a : ι) → α) i : α) (0 : α) ↔
    Eq.{u_2 + 1} (α := Finset α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α) (0 : Finset α)
⊢ i ∈ f.support ∪ g.support ↔
    Ne.{u_2 + 1} (α := Finset α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α) (0 : Finset α)

Tactic:
rw [mem_union, ← not_iff_not, not_or, notMem_support_iff, notMem_support_iff, not_ne_iff]

Premises used: not_iff_not, Finsupp.notMem_support_iff, not_ne_iff, not_or, Finset.mem_union
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
f_1 g_1 : ι →₀ α
i_1 : ι
a : α
f g : ι →₀ α
i : ι
⊢ Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ∧ Eq.{u_2 + 1} (α := α) ((g : (a : ι) → α) i : α) (0 : α) ↔
    Eq.{u_2 + 1} (α := Finset α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α) (0 : Finset α)

Tactic:
Icc_eq_singleton_iff.symm

Premises used: Finset.Icc_eq_singleton_iff, Iff.symm
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
f_1 g_1 : ι →₀ α
i_1 : ι
a : α
f g : ι →₀ α
i : ι
⊢ Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ∧ Eq.{u_2 + 1} (α := α) ((g : (a : ι) → α) i : α) (0 : α) ↔
    Eq.{u_2 + 1} (α := Finset α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α) (0 : Finset α)

Tactic:
exact Icc_eq_singleton_iff.symm

Premises used: Finset.Icc_eq_singleton_iff, Iff.symm
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
i : ι
f g : ι →₀ α
⊢ Eq.{u_2 + 1} (α := Finset α) ((f.rangeIcc g : (a : ι) → Finset α) i : Finset α)
    (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)

Tactic:
rfl

Premises used: Finset.Icc, rfl
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
f g : ι →₀ α
⊢ (f.rangeIcc g).support = f.support ∪ g.support

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
f g : ι →₀ α
i : ι
a : α
⊢ Membership.mem (γ := Finset α) ((f.rangeIcc g : (a : ι) → Finset α) i : Finset α) a ↔
    (f : (a : ι) → α) i ≤ a ∧ a ≤ (g : (a : ι) → α) i

Tactic:
mem_Icc

Premises used: Set.Mem, setOf, Finset.mem_Icc
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f_1 g_1 f g x : ι →₀ α
⊢ Membership.mem (γ := Finset (ι →₀ α))
      ((fun (f g : ι →₀ α) ↦ ((f.support ∪ g.support).finsupp (⇑(f.rangeIcc g) : (a : ι) → Finset α) : Finset (ι →₀ α)))
        f g)
      x ↔
    f ≤ x ∧ x ≤ g

Tactic:
(mem_finsupp_iff_of_support_subset <| Finset.subset_of_eq <| rangeIcc_support _ _).trans ?_

Premises used: Set.Mem, setOf, Finset.mem_finsupp_iff_of_support_subset, Iff.trans, Finsupp.rangeIcc_support, Finset.subset_of_eq
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f_1 g_1 f g x : ι →₀ α
rangeIcc_support :
  (∀ (i : ι),
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((f.rangeIcc g : (a : ι) → Finset α) i : Finset α)
        ((x : (a : ι) → α) i : α)) ↔
    f ≤ x ∧ x ≤ g
⊢ Membership.mem (γ := Finset (ι →₀ α))
      ((fun (f g : ι →₀ α) ↦ ((f.support ∪ g.support).finsupp (⇑(f.rangeIcc g) : (a : ι) → Finset α) : Finset (ι →₀ α)))
        f g)
      x ↔
    f ≤ x ∧ x ≤ g

Tactic:
refine
        (mem_finsupp_iff_of_support_subset <| Finset.subset_of_eq <| rangeIcc_support _ _).trans ?_

Premises used: Finset.mem_finsupp_iff_of_support_subset, Iff.trans, Finsupp.rangeIcc_support, Finset.subset_of_eq
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f_1 g_1 f g x : ι →₀ α
simp_rw :
  (∀ (i : ι),
      LE.le.{u_2} (α := α) ((f : (a : ι) → α) i : α) ((x : (a : ι) → α) i : α) ∧
        LE.le.{u_2} (α := α) ((x : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)) ↔
    f ≤ x ∧ x ≤ g
⊢ (∀ (i : ι),
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((f.rangeIcc g : (a : ι) → Finset α) i : Finset α)
        ((x : (a : ι) → α) i : α)) ↔
    f ≤ x ∧ x ≤ g

Tactic:
simp_rw [mem_rangeIcc_apply_iff]

Premises used: Finsupp.mem_rangeIcc_apply_iff
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f_1 g_1 f g x : ι →₀ α
⊢ (∀ (i : ι),
      LE.le.{u_2} (α := α) ((f : (a : ι) → α) i : α) ((x : (a : ι) → α) i : α) ∧
        LE.le.{u_2} (α := α) ((x : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)) ↔
    f ≤ x ∧ x ≤ g

Tactic:
forall_and

Premises used: forall_and
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f_1 g_1 f g x : ι →₀ α
⊢ (∀ (i : ι),
      LE.le.{u_2} (α := α) ((f : (a : ι) → α) i : α) ((x : (a : ι) → α) i : α) ∧
        LE.le.{u_2} (α := α) ((x : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)) ↔
    f ≤ x ∧ x ≤ g

Tactic:
exact forall_and

Premises used: forall_and
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
⊢ Icc f g = (f.support ∪ g.support).finsupp (⇑(f.rangeIcc g) : (a : ι) → Finset α)

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, Finset.finsupp, rfl
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
simp_rw :
  card (α := ι →₀ α) ((f.support ∪ g.support).finsupp (⇑(f.rangeIcc g) : (a : ι) → Finset α)) =
    ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
simp_rw₁ :
  Eq (α := ℕ) (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) ((f.rangeIcc g : (a : ι) → Finset α) i))
    (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α))
⊢ #(Icc f g) =
    ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)

Tactic:
simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]

Premises used: Finsupp.coe_rangeIcc, Finsupp.Icc_eq, Finset.card_finsupp
-- Module: Mathlib.Data.Finsupp.Interval
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
rw₁ 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
⊢ #(Ico f g) =
    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]

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

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

Premises used: Finset.card_Ioo_eq_card_Icc_sub_two, Finsupp.card_Icc
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Lattice α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
f g : ι →₀ α
rw :
  #(uIcc f g) =
    ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support,
      card.{u_2} (α := α) (uIcc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
⊢ #(uIcc f g) =
    ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (uIcc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)

Tactic:
rw [← support_inf_union_support_sup]

Premises used: Finsupp.support_inf_union_support_sup
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Lattice α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) =
    ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support,
      card.{u_2} (α := α) (uIcc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)

Tactic:
card_Icc (_ : ι →₀ α) _

Premises used: Finsupp.card_Icc, Finset.uIcc
-- Module: Mathlib.Data.Finsupp.Interval
Goal:
ι : Type u_1
α : Type u_2
inst : Lattice α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) =
    ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support,
      card.{u_2} (α := α) (uIcc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)

Tactic:
exact card_Icc (_ : ι →₀ α) _

Premises used: Finsupp.card_Icc
-- Module: Mathlib.Data.Finsupp.Interval
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 : ι →₀ α
⊢ #(Iic f) = ∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)

Tactic:
simp [Iic_eq_Icc, card_Icc, bot_eq_zero]

Premises used: Finsupp.card_Icc, Finset.Iic_eq_Icc, bot_eq_zero
-- Module: Mathlib.Data.Finsupp.Interval
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 : ι →₀ α
⊢ #(Iic f) = ∏ i ∈ f.support, card.{u_2} (α := α) (Iic ((f : (a : ι) → α) i) : Finset α)

Tactic:
classical simp [Iic_eq_Icc, card_Icc, bot_eq_zero]

Premises used: Finsupp.card_Icc, Finset.Iic_eq_Icc, bot_eq_zero
-- Module: Mathlib.Data.Finsupp.Interval
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
rw₁ 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
⊢ #(Iio f) = 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]

Premises used: Finset.card_Iio_eq_card_Iic_sub_one, Finsupp.card_Iic
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := α) (β := DegLex α) (⇑toDegLex : (a : α) → DegLex α)

Tactic:
fun _ _ ↦ _root_.id

Premises used: id, DegLex, Function.Injective
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
a b : α
⊢ Eq (α := DegLex α) ((toDegLex : (a : α) → DegLex α) a : DegLex α) ((toDegLex : (a : α) → DegLex α) b : DegLex α) ↔
    a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, DegLex
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := DegLex α) (β := α) (⇑ofDegLex : (a : DegLex α) → α)

Tactic:
fun _ _ ↦ _root_.id

Premises used: id, DegLex, Function.Injective
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
a b : DegLex α
⊢ Eq (α := α) ((ofDegLex : (a : DegLex α) → α) a : α) ((ofDegLex : (a : DegLex α) → α) b : α) ↔ a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, DegLex
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ DegLex α) (Equiv.symm ofDegLex) toDegLex

Tactic:
rfl

Premises used: toDegLex, DegLex, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := DegLex α ≃ α) (Equiv.symm toDegLex) ofDegLex

Tactic:
rfl

Premises used: ofDegLex, DegLex, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
a : α
⊢ (ofDegLex : (a : DegLex α) → α) ((toDegLex : (a : α) → DegLex α) a : DegLex α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
a : DegLex α
⊢ (toDegLex : (a : α) → DegLex α) ((ofDegLex : (a : DegLex α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
p : DegLex α → Prop
⊢ (∀ (a : DegLex α), p a) ↔ ∀ (a : α), p ((toDegLex : (a : α) → DegLex α) a)

Tactic:
Iff.rfl

Premises used: Iff.rfl, DegLex
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
p : DegLex α → Prop
⊢ (∃ (a : DegLex α), p a) ↔ ∃ (a : α), p ((toDegLex : (a : α) → DegLex α) a)

Tactic:
Iff.rfl

Premises used: Iff.rfl, DegLex
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : AddCommMonoid α
a b : α
⊢ (toDegLex : (a : α) → DegLex α) (a + b) =
    HAdd.hAdd (α := DegLex α) (β := DegLex α) ((toDegLex : (a : α) → DegLex α) a : DegLex α)
      ((toDegLex : (a : α) → DegLex α) b : DegLex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : AddCommMonoid α
a b : DegLex α
⊢ (ofDegLex : (a : DegLex α) → α) (a + b) =
    HAdd.hAdd (α := α) (β := α) ((ofDegLex : (a : DegLex α) → α) a : α) ((ofDegLex : (a : DegLex α) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
r : α → α → Prop
s : ℕ → ℕ → Prop
a b : α →₀ ℕ
⊢ Finsupp.DegLex r s a b ↔
    Prod.Lex (β := α →₀ ℕ) s (Finsupp.Lex r s) ((degree : (a : α →₀ ℕ) → ℕ) a, a) ((degree : (a : α →₀ ℕ) → ℕ) b, b)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Finsupp.DegLex
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 (α := ℕ × (α →₀ ℕ)) (Prod.Lex s (Finsupp.Lex r s))

Tactic:
have wft := WellFounded.prod_lex hs (Finsupp.Lex.wellFounded' hs0 hs hr)
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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))
⊢ Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) Set.univ (Prod.Lex s (Finsupp.Lex r s))

Tactic:
rw [← Set.wellFoundedOn_univ] at wft

Premises used: Set.wellFoundedOn_univ