feat(order/locally_finite): add lemmas expanding finset.Icc (#16996)

This avoids the need to unfold `finset.Icc` to access the component-wise definitions.

I only really needed this for `prod`, but added a handful of lemmas elsewhere too.

src/data/dfinsupp/interval.lean

@@ -152,6 +152,8 @@ locally_finite_order.of_Icc (Π₀ i, α i)
 
 variables (f g : Π₀ i, α i)
 
+lemma Icc_eq : Icc f g = (f.support ∪ g.support).dfinsupp (f.range_Icc g) := rfl
+
 lemma card_Icc : (Icc f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card :=
 card_dfinsupp _ _
 

src/data/finsupp/interval.lean

@@ -75,6 +75,8 @@ locally_finite_order.of_Icc (ι →₀ α)
     exact forall_and_distrib,
   end)
 
+lemma Icc_eq : Icc f g = (f.support ∪ g.support).finsupp (f.range_Icc g) := rfl
+
 lemma card_Icc : (Icc f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card :=
 card_finsupp _ _
 

src/data/pi/interval.lean

@@ -28,6 +28,8 @@ locally_finite_order.of_Icc _
 
 variables (a b : Π i, α i)
 
+lemma Icc_eq : Icc a b = pi_finset (λ i, Icc (a i) (b i)) := rfl
+
 lemma card_Icc : (Icc a b).card = ∏ i, (Icc (a i) (b i)).card := card_pi_finset _
 
 lemma card_Ico : (Ico a b).card = (∏ i, (Icc (a i) (b i)).card) - 1 :=

src/order/locally_finite.lean

@@ -656,6 +656,8 @@ lemma Iio_of_dual (a : αᵒᵈ) : Iio (of_dual a) = (Ioi a).map of_dual.to_embe
 
 end locally_finite_order_top
 
+namespace prod
+
 instance [locally_finite_order α] [locally_finite_order β]
   [decidable_rel ((≤) : α × β → α × β → Prop)] :
   locally_finite_order (α × β) :=
@@ -675,6 +677,21 @@ instance [locally_finite_order_bot α] [locally_finite_order_bot β]
 locally_finite_order_bot.of_Iic' (α × β)
   (λ a, Iic a.fst ×ˢ Iic a.snd) (λ a x, by { rw [mem_product, mem_Iic, mem_Iic], refl })
 
+lemma Icc_eq [locally_finite_order α] [locally_finite_order β]
+  [decidable_rel ((≤) : α × β → α × β → Prop)] (p q : α × β) :
+  finset.Icc p q = finset.Icc p.1 q.1 ×ˢ finset.Icc p.2 q.2 := rfl
+
+@[simp] lemma Icc_mk_mk [locally_finite_order α] [locally_finite_order β]
+  [decidable_rel ((≤) : α × β → α × β → Prop)] (a₁ a₂ : α) (b₁ b₂ : β) :
+  finset.Icc (a₁, b₁) (a₂, b₂) = finset.Icc a₁ a₂ ×ˢ finset.Icc b₁ b₂ := rfl
+
+lemma card_Icc [locally_finite_order α] [locally_finite_order β]
+  [decidable_rel ((≤) : α × β → α × β → Prop)] (p q : α × β) :
+  (finset.Icc p q).card = (finset.Icc p.1 q.1).card * (finset.Icc p.2 q.2).card :=
+finset.card_product _ _
+
+end prod
+
 end preorder
 
 /-!