[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LE (α i)
⊢ ∀ {a b : Π₀ (i : ι), α i},
    ↑{ toFun := FunLike.coe, inj' := (_ : Function.Injective fun f => ↑f) } a ≤
        ↑{ toFun := FunLike.coe, inj' := (_ : Function.Injective fun f => ↑f) } b ↔
      a ≤ b
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (↑(support (f ⊓ g) ∪ support (f ⊔ g)))ᶜ = (↑(support f ∪ support g))ᶜ
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x✝ : ι
⊢ x✝ ∈ (↑(support (f ⊓ g) ∪ support (f ⊔ g)))ᶜ ↔ x✝ ∈ (↑(support f ∪ support g))ᶜ
[PROOFSTEP]
simp [inf_eq_and_sup_eq_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
⊢ ∀ (a : Π₀ (i : ι), α i), ⊥ ≤ a
[PROOFSTEP]
simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
f g : Π₀ (i : ι), α i
⊢ f + g = 0 ↔ f = 0 ∧ g = 0
[PROOFSTEP]
simp [FunLike.ext_iff, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
s : Finset ι
i : ι
a : α i
⊢ (∀ (i_1 : ι), i_1 ∈ {i} → ↑(single i a) i_1 ≤ ↑f i_1) ↔ a ≤ ↑f i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i : ι
a b : α i
f g : Π₀ (i : ι), α i
⊢ ↑(f - g) = ↑f - ↑g
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a b : α i✝
f g : Π₀ (i : ι), α i
i : ι
⊢ ↑(f - g) i = (↑f - ↑g) i
[PROOFSTEP]
exact tsub_apply f g i
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
⊢ ∀ {a b : Π₀ (i : ι), α i}, a ≤ b → ∃ c, b = a + c
[PROOFSTEP]
intro f g h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i : ι
a b : α i
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
f g : Π₀ (i : ι), α i
h : f ≤ g
⊢ ∃ c, g = f + c
[PROOFSTEP]
exists g - f
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i : ι
a b : α i
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
f g : Π₀ (i : ι), α i
h : f ≤ g
⊢ g = f + (g - f)
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a b : α i✝
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
f g : Π₀ (i : ι), α i
h : f ≤ g
i : ι
⊢ ↑g i = ↑(f + (g - f)) i
[PROOFSTEP]
exact (add_tsub_cancel_of_le <| h i).symm
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ single i (a - b) = single i a - single i b
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
obtain rfl | h := eq_or_ne i j
[GOAL]
case h.inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ ↑(single i (a - b)) i = ↑(single i a - single i b) i
[PROOFSTEP]
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
[GOAL]
case h.inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : i ≠ j
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ support (f - g) ⊆ support f
[PROOFSTEP]
simp (config := { contextual := true }) only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff, Ne.def, coe_tsub,
  Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ support f \ support g ⊆ support (f - g)
[PROOFSTEP]
simp (config := { contextual := true }) [subset_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support (f ⊓ g) = support f ∩ support g
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ support (f ⊓ g) ↔ a✝ ∈ support f ∩ support g
[PROOFSTEP]
simp only [inf_apply, mem_support_iff, Ne.def, Finset.mem_inter]
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬↑f a✝ ⊓ ↑g a✝ = 0 ↔ ¬↑f a✝ = 0 ∧ ¬↑g a✝ = 0
[PROOFSTEP]
simp only [inf_eq_min, ← nonpos_iff_eq_zero, min_le_iff, not_or]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support (f ⊔ g) = support f ∪ support g
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ support (f ⊔ g) ↔ a✝ ∈ support f ∪ support g
[PROOFSTEP]
simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne.def, ← bot_eq_zero]
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
[PROOFSTEP]
rw [_root_.sup_eq_bot_iff, not_and_or]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ Disjoint f g ↔ Disjoint (support f) (support g)
[PROOFSTEP]
rw [disjoint_iff, disjoint_iff, DFinsupp.bot_eq_zero, ← DFinsupp.support_eq_empty, DFinsupp.support_inf]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support f ∩ support g = ∅ ↔ support f ⊓ support g = ⊥
[PROOFSTEP]
rfl
