[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ Function.Injective fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)
[PROOFSTEP]
refine' (mk_injective _).comp fun f g h => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f✝ : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h : (fun i => f ↑i (_ : ↑i ∈ ↑s)) = fun i => g ↑i (_ : ↑i ∈ ↑s)
⊢ f = g
[PROOFSTEP]
ext i hi
[GOAL]
case h.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f✝ : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h : (fun i => f ↑i (_ : ↑i ∈ ↑s)) = fun i => g ↑i (_ : ↑i ∈ ↑s)
i : ι
hi : i ∈ s
⊢ f i hi = g i hi
[PROOFSTEP]
convert congr_fun h ⟨i, hi⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ f ∈ dfinsupp s t ↔ support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
[PROOFSTEP]
refine' mem_map.trans ⟨_, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (∃ a,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f) →
    support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
[PROOFSTEP]
rintro ⟨f, hf, rfl⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
⊢ support
        (↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          f) ⊆
      s ∧
    ∀ (i : ι),
      i ∈ s →
        ↑(↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                    inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
                f)
            i ∈
          t i
[PROOFSTEP]
rw [Function.Embedding.coeFn_mk]
  -- porting note: added to avoid heartbeat timeout
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
⊢ support (DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) ⊆ s ∧
    ∀ (i : ι), i ∈ s → ↑(DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
[PROOFSTEP]
refine' ⟨support_mk_subset, fun i hi => _⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
[PROOFSTEP]
convert mem_pi.1 hf i hi
[GOAL]
case h.e'_4
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i = f i hi
[PROOFSTEP]
exact mk_of_mem hi
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i) →
    ∃ a,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f
[PROOFSTEP]
refine' fun h => ⟨fun i _ => f i, mem_pi.2 h.2, _⟩
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
⊢ (↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
          inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
      fun i x => ↑f i) =
    f
[PROOFSTEP]
ext i
[GOAL]
case refine'_2.h
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ ↑(↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          fun i x => ↑f i)
      i =
    ↑f i
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.h
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ (if i ∈ s then ↑f i else 0) = ↑f i
[PROOFSTEP]
exact ite_eq_left_iff.2 fun hi => (not_mem_support_iff.1 fun H => hi <| h.1 H).symm
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
⊢ f ∈ dfinsupp s ↑t ↔ ∀ (i : ι), ↑f i ∈ ↑t i
[PROOFSTEP]
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⟩⟩)
[GOAL]
case refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
by_cases hi : i ∈ s
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
exact h.2 hi
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
rw [not_mem_support_iff.1 (mt h.1 hi), not_mem_support_iff.1 (not_mem_mono ht hi)]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ 0 ∈ 0
[PROOFSTEP]
exact zero_mem_zero
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : ↑f i ∈ ↑t i
hi : i ∈ support f
H : ↑t i = 0
⊢ ↑f i = 0
[PROOFSTEP]
rwa [H, mem_zero] at h 
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
⊢ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
have hf : f i = 0 :=
  (fs.prop i).resolve_left (Multiset.not_mem_mono (Multiset.Le.subset <| Multiset.le_add_right _ _) h)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
hf : ↑f i = 0
⊢ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
have hg : g i = 0 :=
  (gs.prop i).resolve_left
    (Multiset.not_mem_mono (Multiset.Le.subset <| Multiset.le_add_left _ _) h)
      -- porting note: was rw, but was rewriting under lambda, so changed to simp_rw
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
hf : ↑f i = 0
hg : ↑g i = 0
⊢ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
simp_rw [hf, hg]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
hf : ↑f i = 0
hg : ↑g i = 0
⊢ Icc 0 0 = 0
[PROOFSTEP]
exact Icc_self _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
⊢ support (rangeIcc f g) ⊆ support f ∪ support g
[PROOFSTEP]
refine' fun x hx => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
⊢ x ∈ support f ∪ support g
[PROOFSTEP]
by_contra h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
h : ¬x ∈ support f ∪ support g
⊢ False
[PROOFSTEP]
refine' not_mem_support_iff.2 _ hx
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
h : ¬x ∈ support f ∪ support g
⊢ ↑(rangeIcc f g) x = 0
[PROOFSTEP]
rw [rangeIcc_apply, not_mem_support_iff.1 (not_mem_mono (subset_union_left _ _) h),
  not_mem_support_iff.1 (not_mem_mono (subset_union_right _ _) h)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
h : ¬x ∈ support f ∪ support g
⊢ Icc 0 0 = 0
[PROOFSTEP]
exact Icc_self _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ card (pi f) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
rw [pi, card_dfinsupp]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i in support f, card (↑f i) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
i : ι
x✝ : i ∈ support f
⊢ card (↑f i) = (fun i => ↑(card (↑f i))) i (↑f i)
[PROOFSTEP]
simp only [Pi.nat_apply, Nat.cast_id]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ x ∈ (fun f g => dfinsupp (support f ∪ support g) ↑(rangeIcc f g)) f g ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
refine' (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), ↑x i ∈ ↑(rangeIcc f g) i) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
simp_rw [mem_rangeIcc_apply_iff, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ ((∀ (x_1 : ι), ↑f x_1 ≤ ↑x x_1) ∧ ∀ (x_1 : ι), ↑x x_1 ≤ ↑g x_1) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (Ico f g) = ∏ i in support f ∪ support g, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (Ioc f g) = ∏ i in support f ∪ support g, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (Ioo f g) = ∏ i in support f ∪ support g, card (Icc (↑f i) (↑g i)) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (uIcc f g) = ∏ i in support f ∪ support g, card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
rw [← support_inf_union_support_sup]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (uIcc f g) = ∏ i in support (f ⊓ g) ∪ support (f ⊔ g), card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
exact card_Icc _ _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ card (Iic f) = ∏ i in support f, card (Iic (↑f i))
[PROOFSTEP]
simp_rw [Iic_eq_Icc, card_Icc, DFinsupp.bot_eq_zero, support_zero, empty_union, zero_apply, bot_eq_zero]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ card (Iio f) = ∏ i in support f, card (Iic (↑f i)) - 1
[PROOFSTEP]
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
