awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
refine_2 :
  ∀ (h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i),
    (({
            toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
              DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
            inj' := ⋯ } :
          (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
        fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i) =
      f
⊢ (f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i) →
    ∃ a ∈ s.pi (β := α) t,
      ({
              toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
              inj' := ⋯ } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          a =
        f

Tactic:
refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
refine_2 :
  ∀ (i : ι),
    (({
                toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                  DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
                inj' := ⋯ : ((a : ι) → a ∈ s → α a) ↪ Π₀ (i : ι), α i } :
              (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
            fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i :
          (a : ι) → α a)
        i =
      (f : (a : ι) → α a) i
⊢ (({
          toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
            DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
          inj' := ⋯ } :
        (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
      fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i) =
    f

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
i : ι
refine_2 : (if i ∈ s then (f : (a : ι) → α a) i else 0) = (f : (a : ι) → α a) i
⊢ (({
              toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
              inj' := ⋯ : ((a : ι) → a ∈ s → α a) ↪ Π₀ (i : ι), α i } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i :
        (a : ι) → α a)
      i =
    (f : (a : ι) → α a) i

Tactic:
dsimp
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
i : ι
⊢ (if i ∈ s then (f : (a : ι) → α a) i else 0) = (f : (a : ι) → α a) i

Tactic:
ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

Premises used: Iff.mpr, ite_eq_left_iff, DFinsupp.notMem_support_iff, And.left, Iff.mp, Eq.symm
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
i : ι
⊢ (if i ∈ s then (f : (a : ι) → α a) i else 0) = (f : (a : ι) → α a) i

Tactic:
exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

Premises used: Iff.mpr, ite_eq_left_iff, DFinsupp.notMem_support_iff, And.left, Iff.mp, Eq.symm
-- Module: Mathlib.Data.DFinsupp.Interval
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
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i)) (s.dfinsupp (α := α) (⇑t : (a : ι) → Finset (α a))) f ↔
    ∀ (i : ι), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i

Tactic:
mem_dfinsupp_iff.trans (forall_and.symm.trans <| forall_congr' fun i =>
      ⟨ fun h => ?_,
        fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)

Premises used: Iff.mpr, DFinsupp.mem_support_iff, And.intro, Iff.intro, Iff.mp, forall_congr', Iff.trans, Iff.symm, Finset.mem_dfinsupp_iff, forall_and
-- Module: Mathlib.Data.DFinsupp.Interval
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
refine_1 :
  ∀ (i : ι) (h : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)),
    (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
refine_2 :
  ∀ (i : ι) (h : (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i) (hi : i ∈ f.support (β := α))
    (H : (t : (a : ι) → Finset (α a)) i = 0), (f : (a : ι) → α a) i = 0
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i)) (s.dfinsupp (α := α) (⇑t : (a : ι) → Finset (α a))) f ↔
    ∀ (i : ι), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i

Tactic:
refine mem_dfinsupp_iff.trans (forall_and.symm.trans <| forall_congr' fun i =>
      ⟨ fun h => ?_,
        fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)

Premises used: Iff.mpr, DFinsupp.mem_support_iff, And.intro, Iff.intro, Iff.mp, forall_congr', Iff.trans, Iff.symm, Finset.mem_dfinsupp_iff, forall_and
-- Module: Mathlib.Data.DFinsupp.Interval
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 : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
pos : ∀ (hi : i ∈ s), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
neg : ∀ (hi : i ∉ s), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
⊢ (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Data.DFinsupp.Interval
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 : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
hi : i ∈ s
⊢ (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i

Tactic:
h.2 hi

Premises used: And.right
-- Module: Mathlib.Data.DFinsupp.Interval
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 : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
hi : i ∈ s
⊢ (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i

Tactic:
exact h.2 hi

Premises used: And.right
-- Module: Mathlib.Data.DFinsupp.Interval
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 : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
hi : i ∉ s
neg : Membership.mem (γ := Finset (α i)) 0 0
⊢ (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i

Tactic:
rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 (notMem_mono ht hi)]

Premises used: DFinsupp.notMem_support_iff, mt, And.left, Iff.mp, Finset.notMem_mono
-- Module: Mathlib.Data.DFinsupp.Interval
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 : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
hi : i ∉ s
⊢ Membership.mem (γ := Finset (α i)) 0 0

Tactic:
zero_mem_zero

Premises used: Finset.zero_mem_zero
-- Module: Mathlib.Data.DFinsupp.Interval
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 : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
hi : i ∉ s
⊢ Membership.mem (γ := Finset (α i)) 0 0

Tactic:
exact zero_mem_zero

Premises used: Finset.zero_mem_zero
-- Module: Mathlib.Data.DFinsupp.Interval
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
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (h : (f : (a : ι) → α a) i = 0) (hi : i ∈ f.support (β := α)) (H : (t : (a : ι) → Finset (α a)) i = 0),
    (f : (a : ι) → α a) i = 0
⊢ (f : (a : ι) → α a) i = 0

Tactic:
rwa [H, mem_zero] at h

Premises used: Finset.mem_zero
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ a ∈ (f.singleton (α := α) : (a : ι) → Finset (α a)) i ↔ a = (f : (a : ι) → α a) i

Tactic:
mem_singleton

Premises used: Finset.mem_singleton, Set.Mem, setOf
-- Module: Mathlib.Data.DFinsupp.Interval
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 ι)
⊢ (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)
-- Module: Mathlib.Data.DFinsupp.Interval
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
⊢ (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)
-- Module: Mathlib.Data.DFinsupp.Interval
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
simp_rw : Eq.{u_2 + 1} (α := Finset (α i)) (Icc 0 0) 0
⊢ Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i) = 0

Tactic:
simp_rw [hf, hg]
-- Module: Mathlib.Data.DFinsupp.Interval
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
⊢ Eq.{u_2 + 1} (α := Finset (α i)) (Icc 0 0) 0

Tactic:
Icc_self _

Premises used: Finset.Icc_self
-- Module: Mathlib.Data.DFinsupp.Interval
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
⊢ Eq.{u_2 + 1} (α := Finset (α i)) (Icc 0 0) 0

Tactic:
exact Icc_self _

Premises used: Finset.Icc_self
-- Module: Mathlib.Data.DFinsupp.Interval
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
i : ι
⊢ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) i = Icc ((f : (a : ι) → α a) i) ((g : (a : ι) → α a) i)

Tactic:
rfl

Premises used: Finset.Icc, rfl
-- Module: Mathlib.Data.DFinsupp.Interval
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
i : ι
a : α i
⊢ a ∈ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) i ↔ (f : (a : ι) → α a) i ≤ a ∧ a ≤ (g : (a : ι) → α a) i

Tactic:
mem_Icc

Premises used: Set.Mem, setOf, Finset.mem_Icc
-- Module: Mathlib.Data.DFinsupp.Interval
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 (β := α)

Tactic:
fun x hx => ?_
-- Module: Mathlib.Data.DFinsupp.Interval
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)
refine :
  ∀ (x : ι) (hx : x ∈ (f.rangeIcc (α := α) g).support (β := fun (i : ι) ↦ Finset (α i))),
    x ∈ f.support (β := α) ∪ g.support (β := α)
⊢ (f.rangeIcc (α := α) g).support (β := fun (i : ι) ↦ Finset (α i)) ⊆ f.support (β := α) ∪ g.support (β := α)

Tactic:
refine fun x hx => ?_
-- Module: Mathlib.Data.DFinsupp.Interval
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))
by_contra : ∀ (h : x ∉ f.support (β := α) ∪ g.support (β := α)), False
⊢ x ∈ f.support (β := α) ∪ g.support (β := α)

Tactic:
by_contra h
-- Module: Mathlib.Data.DFinsupp.Interval
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

Tactic:
notMem_support_iff.2 ?_ hx

Premises used: Iff.mpr, DFinsupp.notMem_support_iff
-- Module: Mathlib.Data.DFinsupp.Interval
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 (β := α)
refine : (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) x = 0
⊢ False

Tactic:
refine notMem_support_iff.2 ?_ hx

Premises used: Iff.mpr, DFinsupp.notMem_support_iff
-- Module: Mathlib.Data.DFinsupp.Interval
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 (β := α)
rw : Eq.{u_2 + 1} (α := Finset (α x)) (Icc 0 0) 0
⊢ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) x = 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)]

Premises used: DFinsupp.notMem_support_iff, Finset.subset_union_left, DFinsupp.rangeIcc_apply, Iff.mp, Finset.notMem_mono, Finset.subset_union_right
-- Module: Mathlib.Data.DFinsupp.Interval
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 (β := α)
⊢ Eq.{u_2 + 1} (α := Finset (α x)) (Icc 0 0) 0

Tactic:
Icc_self _

Premises used: Finset.Icc_self
-- Module: Mathlib.Data.DFinsupp.Interval
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 (β := α)
⊢ Eq.{u_2 + 1} (α := Finset (α x)) (Icc 0 0) 0

Tactic:
exact Icc_self _

Premises used: Finset.Icc_self
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
g : Π₀ (i : ι), α i
⊢ g ∈ f.pi (α := α) ↔ ∀ (i : ι), (g : (a : ι) → α a) i ∈ (f : (a : ι) → Finset (α a)) i

Tactic:
mem_dfinsupp_iff_of_support_subset <| Subset.refl _

Premises used: Finset.mem_dfinsupp_iff_of_support_subset, Set.Mem, Finset.Subset.refl, setOf
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
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) → ℕ))
⊢ #(f.pi (α := α)) =
    f.prod (β := fun (i : ι) ↦ Finset (α i)) fun (i : ι) ↦ (↑(#((f : (a : ι) → Finset (α a)) i)) : Finset (α i) → ℕ)

Tactic:
rw [pi, card_dfinsupp]

Premises used: Finset.card_dfinsupp, DFinsupp.pi
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
i : ι
h : i ∈ f.support (β := fun (i : ι) ↦ Finset (α i))
⊢ #((f : (a : ι) → Finset (α a)) i) =
    (fun (i : ι) ↦ ((↑(#((f : (a : ι) → Finset (α a)) i)) : Finset (α i) → ℕ) : Finset (α i) → ℕ)) i
      ((f : (a : ι) → Finset (α a)) i)

Tactic:
simp only [Pi.natCast_apply, Nat.cast_id]

Premises used: Nat.cast_id, Pi.natCast_apply
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ 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:
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

Premises used: Finset.prod_congr, rfl
-- 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 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

Tactic:
(mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans ?_

Premises used: Finset.mem_dfinsupp_iff_of_support_subset, Set.Mem, setOf, DFinsupp.support_rangeIcc_subset, Iff.trans
-- 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 x : Π₀ (i : ι), α i
refine : (∀ (i : ι), (x : (a : ι) → α a) i ∈ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) i) ↔ f ≤ x ∧ x ≤ g
⊢ 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

Tactic:
refine (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans ?_

Premises used: Finset.mem_dfinsupp_iff_of_support_subset, DFinsupp.support_rangeIcc_subset, Iff.trans
-- 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 x : Π₀ (i : ι), α i
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
⊢ (∀ (i : ι), (x : (a : ι) → α a) i ∈ (f.rangeIcc (α := α) g : (a : ι) → Finset (α a)) i) ↔ f ≤ x ∧ x ≤ g

Tactic:
simp_rw [mem_rangeIcc_apply_iff, forall_and]

Premises used: DFinsupp.mem_rangeIcc_apply_iff, forall_and
-- 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 x : Π₀ (i : ι), α i
⊢ ((∀ (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:
rfl
-- 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 =
    (f.support (β := α) ∪ g.support (β := α)).dfinsupp (α := α) (⇑(f.rangeIcc (α := α) g) : (a : ι) → Finset (α a))

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, Finset.dfinsupp, rfl