Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore: tidy various files #2056

Closed
wants to merge 1 commit into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
86 changes: 38 additions & 48 deletions Mathlib/Data/Finsupp/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,6 @@ structure Finsupp (α : Type _) (M : Type _) [Zero M] where
#align finsupp.to_fun Finsupp.toFun
#align finsupp.mem_support_to_fun Finsupp.mem_support_toFun

-- mathport name: «expr →₀ »
@[inherit_doc]
infixr:25 " →₀ " => Finsupp

Expand Down Expand Up @@ -163,7 +162,7 @@ theorem coe_mk (f : α → M) (s : Finset α) (h : ∀ a, a ∈ s ↔ f a ≠ 0)
rfl
#align finsupp.coe_mk Finsupp.coe_mk

instance hasZero: Zero (α →₀ M) :=
instance zero : Zero (α →₀ M) :=
⟨⟨∅, 0, fun _ => ⟨fun h ↦ (not_mem_empty _ h).elim, fun H => (H rfl).elim⟩⟩⟩

@[simp]
Expand Down Expand Up @@ -244,8 +243,7 @@ theorem support_subset_iff {s : Set α} {f : α →₀ M} : ↑f.support ⊆ s
/-- Given `Finite α`, `equivFunOnFinite` is the `Equiv` between `α →₀ β` and `α → β`.
(All functions on a finite type are finitely supported.) -/
@[simps]
def equivFunOnFinite [Finite α] : (α →₀ M) ≃ (α → M)
where
def equivFunOnFinite [Finite α] : (α →₀ M) ≃ (α → M) where
toFun := (⇑)
invFun f := mk (Function.support f).toFinite.toFinset f fun _a => Set.Finite.mem_toFinset _
left_inv _f := ext fun _x => rfl
Expand Down Expand Up @@ -532,27 +530,26 @@ If `b = 0`, this amounts to removing `a` from the `Finsupp.support`.
Otherwise, if `a` was not in the `Finsupp.support`, it is added to it.

This is the finitely-supported version of `Function.update`. -/
def update (f : α →₀ M) (a : α) (b : M) : α →₀ M
where
def update (f : α →₀ M) (a : α) (b : M) : α →₀ M where
support := by
haveI := Classical.decEq α; haveI := Classical.decEq M;
exact if b = 0 then f.support.erase a else insert a f.support
haveI := Classical.decEq α; haveI := Classical.decEq M
exact if b = 0 then f.support.erase a else insert a f.support
toFun :=
haveI := Classical.decEq α
Function.update f a b
mem_support_toFun i := by
classical
simp [Function.update, Ne.def]
split_ifs with hb ha ha <;>
simp [*, Finset.mem_erase]
rw [Finset.mem_erase]
simp
rw [Finset.mem_erase]
simp [ha]
rw [Finset.mem_insert]
simp [ha]
rw [Finset.mem_insert]
simp [ha]
simp only [*, not_false_iff, iff_true, not_true, iff_false]
· rw [Finset.mem_erase]
simp
· rw [Finset.mem_erase]
simp [ha]
· rw [Finset.mem_insert]
simp [ha]
· rw [Finset.mem_insert]
simp [ha]
#align finsupp.update Finsupp.update

@[simp]
Expand Down Expand Up @@ -675,7 +672,7 @@ theorem erase_zero (a : α) : erase a (0 : α →₀ M) = 0 := by

end Erase

/-! ### Declarations about `on_finset` -/
/-! ### Declarations about `onFinset` -/


section OnFinset
Expand Down Expand Up @@ -723,8 +720,7 @@ section OfSupportFinite
variable [Zero M]

/-- The natural `Finsupp` induced by the function `f` given that it has finite support. -/
noncomputable def ofSupportFinite (f : α → M) (hf : (Function.support f).Finite) : α →₀ M
where
noncomputable def ofSupportFinite (f : α → M) (hf : (Function.support f).Finite) : α →₀ M where
support := hf.toFinset
toFun := f
mem_support_toFun _ := hf.mem_toFinset
Expand All @@ -741,14 +737,14 @@ instance canLift : CanLift (α → M) (α →₀ M) (⇑) fun f => (Function.sup

end OfSupportFinite

/-! ### Declarations about `map_range` -/
/-! ### Declarations about `mapRange` -/


section MapRange

variable [Zero M] [Zero N] [Zero P]

/-- The composition of `f : M → N` and `g : α →₀ M` is `map_range f hf g : α →₀ N`,
/-- The composition of `f : M → N` and `g : α →₀ M` is `mapRange f hf g : α →₀ N`,
which is well-defined when `f 0 = 0`.

This preserves the structure on `f`, and exists in various bundled forms for when `f` is itself
Expand Down Expand Up @@ -808,7 +804,7 @@ theorem support_mapRange_of_injective {e : M → N} (he0 : e 0 = 0) (f : ι →

end MapRange

/-! ### Declarations about `emb_domain` -/
/-! ### Declarations about `embDomain` -/


section EmbDomain
Expand All @@ -818,8 +814,7 @@ variable [Zero M] [Zero N]
/-- Given `f : α ↪ β` and `v : α →₀ M`, `Finsupp.embDomain f v : β →₀ M`
is the finitely supported function whose value at `f a : β` is `v a`.
For a `b : β` outside the range of `f`, it is zero. -/
def embDomain (f : α ↪ β) (v : α →₀ M) : β →₀ M
where
def embDomain (f : α ↪ β) (v : α →₀ M) : β →₀ M where
support := v.support.map f
toFun a₂ :=
haveI := Classical.decEq β
Expand Down Expand Up @@ -884,7 +879,7 @@ theorem embDomain_eq_zero {f : α ↪ β} {l : α →₀ M} : embDomain f l = 0
theorem embDomain_mapRange (f : α ↪ β) (g : M → N) (p : α →₀ M) (hg : g 0 = 0) :
embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p) := by
ext a
by_cases a ∈ Set.range f
by_cases h : a ∈ Set.range f
· rcases h with ⟨a', rfl⟩
rw [mapRange_apply, embDomain_apply, embDomain_apply, mapRange_apply]
· rw [mapRange_apply, embDomain_notin_range, embDomain_notin_range, ← hg] <;> assumption
Expand Down Expand Up @@ -925,7 +920,7 @@ theorem embDomain_single (f : α ↪ β) (a : α) (m : M) : embDomain f (single

end EmbDomain

/-! ### Declarations about `zip_with` -/
/-! ### Declarations about `zipWith` -/


section ZipWith
Expand All @@ -937,12 +932,12 @@ variable [Zero M] [Zero N] [Zero P]
`zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, which is well-defined when `f 0 0 = 0`. -/
def zipWith (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) : α →₀ P :=
onFinset
(haveI := Classical.decEq α
g₁.support ∪ g₂.support)
(fun a => f (g₁ a) (g₂ a)) fun a (H : f _ _ ≠ 0) => by
classical
rw [mem_union, mem_support_iff, mem_support_iff, ← not_and_or]
rintro ⟨h₁, h₂⟩; rw [h₁, h₂] at H; exact H hf
(haveI := Classical.decEq α; g₁.support ∪ g₂.support)
(fun a => f (g₁ a) (g₂ a))
fun a (H : f _ _ ≠ 0) => by
classical
rw [mem_union, mem_support_iff, mem_support_iff, ← not_and_or]
rintro ⟨h₁, h₂⟩; rw [h₁, h₂] at H; exact H hf
#align finsupp.zip_with Finsupp.zipWith

@[simp]
Expand All @@ -965,7 +960,7 @@ section AddZeroClass

variable [AddZeroClass M]

instance : Add (α →₀ M) :=
instance add : Add (α →₀ M) :=
⟨zipWith (· + ·) (add_zero 0)⟩

@[simp]
Expand Down Expand Up @@ -1002,7 +997,7 @@ theorem single_add (a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a
· rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add]
#align finsupp.single_add Finsupp.single_add

instance addZeroClass: AddZeroClass (α →₀ M) :=
instance addZeroClass : AddZeroClass (α →₀ M) :=
FunLike.coe_injective.addZeroClass _ coe_zero coe_add

/-- `Finsupp.single` as an `AddMonoidHom`.
Expand All @@ -1020,16 +1015,15 @@ def singleAddHom (a : α) : M →+ α →₀ M where
See `Finsupp.lapply` in `LinearAlgebra/Finsupp` for the stronger version as a linear map. -/
@[simps apply]
def applyAddHom (a : α) : (α →₀ M) →+ M where
toFun := fun g => g a
toFun g := g a
map_zero' := zero_apply
map_add' _ _ := add_apply _ _ _
#align finsupp.apply_add_hom Finsupp.applyAddHom
#align finsupp.apply_add_hom_apply Finsupp.applyAddHom_apply

/-- Coercion from a `Finsupp` to a function type is an `AddMonoidHom`. -/
@[simps]
noncomputable def coeFnAddHom : (α →₀ M) →+ α → M
where
noncomputable def coeFnAddHom : (α →₀ M) →+ α → M where
toFun := (⇑)
map_zero' := coe_zero
map_add' := coe_add
Expand Down Expand Up @@ -1071,8 +1065,7 @@ theorem erase_add (a : α) (f f' : α →₀ M) : erase a (f + f') = erase a f +

/-- `Finsupp.erase` as an `AddMonoidHom`. -/
@[simps]
def eraseAddHom (a : α) : (α →₀ M) →+ α →₀ M
where
def eraseAddHom (a : α) : (α →₀ M) →+ α →₀ M where
toFun := erase a
map_zero' := erase_zero a
map_add' := erase_add a
Expand All @@ -1083,8 +1076,7 @@ protected theorem induction {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 :
(ha : ∀ (a b) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)) : p f :=
suffices ∀ (s) (f : α →₀ M), f.support = s → p f from this _ _ rfl
fun s =>
Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf =>
by
Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf => by
suffices p (single a (f a) + f.erase a) by rwa [single_add_erase] at this
classical
apply ha
Expand All @@ -1100,8 +1092,7 @@ theorem induction₂ {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0)
(ha : ∀ (a b) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)) : p f :=
suffices ∀ (s) (f : α →₀ M), f.support = s → p f from this _ _ rfl
fun s =>
Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf =>
by
Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf => by
suffices p (f.erase a + single a (f a)) by rwa [erase_add_single] at this
classical
apply ha
Expand Down Expand Up @@ -1180,8 +1171,7 @@ theorem mapRange_add' [AddZeroClass N] [AddMonoidHomClass β M N] {f : β} (v₁

/-- Bundle `Finsupp.embDomain f` as an additive map from `α →₀ M` to `β →₀ M`. -/
@[simps]
def embDomain.addMonoidHom (f : α ↪ β) : (α →₀ M) →+ β →₀ M
where
def embDomain.addMonoidHom (f : α ↪ β) : (α →₀ M) →+ β →₀ M where
toFun v := embDomain f v
map_zero' := by simp
map_add' v w := by
Expand Down Expand Up @@ -1211,7 +1201,7 @@ instance hasNatScalar : SMul ℕ (α →₀ M) :=
⟨fun n v => v.mapRange ((· • ·) n) (nsmul_zero _)⟩
#align finsupp.has_nat_scalar Finsupp.hasNatScalar

instance addMonoid: AddMonoid (α →₀ M) :=
instance addMonoid : AddMonoid (α →₀ M) :=
FunLike.coe_injective.addMonoid _ coe_zero coe_add fun _ _ => rfl

end AddMonoid
Expand Down Expand Up @@ -1281,7 +1271,7 @@ instance [AddCommGroup G] : AddCommGroup (α →₀ G) :=
theorem single_add_single_eq_single_add_single [AddCommMonoid M] {k l m n : α} {u v : M}
(hu : u ≠ 0) (hv : v ≠ 0) :
single k u + single l v = single m u + single n v ↔
k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n := by
(k = m ∧ l = n)(u = v ∧ k = n ∧ l = m)(u + v = 0 ∧ k = l ∧ m = n) := by
classical
simp_rw [FunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
exact Pi.single_add_single_eq_single_add_single hu hv
Expand Down
13 changes: 5 additions & 8 deletions Mathlib/Data/Finsupp/Multiset.lean
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import Mathlib.Data.Finsupp.Basic
import Mathlib.Data.Finsupp.Order

/-!
# Equivalence between `multiset` and `ℕ`-valued finitely supported functions
# Equivalence between `Multiset` and `ℕ`-valued finitely supported functions

This defines `Finsupp.toMultiset` the equivalence between `α →₀ ℕ` and `Multiset α`, along
with `Multiset.toFinsupp` the reverse equivalence and `Finsupp.orderIsoMultiset` the equivalence
Expand All @@ -31,13 +31,11 @@ variable {α β ι : Type _}
namespace Finsupp
/-- Given `f : α →₀ ℕ`, `f.toMultiset` is the multiset with multiplicities given by the values of
`f` on the elements of `α`. We define this function as an `AddEquiv`. -/
def toMultiset : (α →₀ ℕ) ≃+ Multiset α
where
def toMultiset : (α →₀ ℕ) ≃+ Multiset α where
toFun f := Finsupp.sum f fun a n => n • {a}
invFun s := ⟨s.toFinset, fun a => s.count a, fun a => by simp⟩
left_inv f :=
ext fun a =>
by
ext fun a => by
simp only [sum, Multiset.count_sum', Multiset.count_singleton, mul_boole, coe_mk,
mem_support_iff, Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
exact Eq.symm
Expand Down Expand Up @@ -198,12 +196,11 @@ theorem Finsupp.toMultiset_toFinsupp (f : α →₀ ℕ) :

namespace Finsupp
/-- `Finsupp.toMultiset` as an order isomorphism. -/
def orderIsoMultiset : (ι →₀ ℕ) ≃o Multiset ι
where
def orderIsoMultiset : (ι →₀ ℕ) ≃o Multiset ι where
toEquiv := toMultiset.toEquiv
map_rel_iff' := by
-- Porting note: This proof used to be simp [Multiset.le_iff_count, le_def]
intro f g;
intro f g
-- Porting note: the following should probably be a simp lemma somewhere;
-- maybe coe_toEquiv in Hom/Equiv/Basic?
have : ⇑ (toMultiset (α := ι)).toEquiv = toMultiset := rfl
Expand Down
13 changes: 6 additions & 7 deletions Mathlib/Data/Finsupp/ToDfinsupp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -71,8 +71,7 @@ variable {ι : Type _} {R : Type _} {M : Type _}
section Defs

/-- Interpret a `Finsupp` as a homogenous `Dfinsupp`. -/
def Finsupp.toDfinsupp [Zero M] (f : ι →₀ M) : Π₀ _i : ι, M
where
def Finsupp.toDfinsupp [Zero M] (f : ι →₀ M) : Π₀ _i : ι, M where
toFun := f
support' :=
Trunc.mk
Expand Down Expand Up @@ -106,7 +105,7 @@ theorem toDfinsupp_support (f : ι →₀ M) : f.toDfinsupp.support = f.support
/-- Interpret a homogenous `Dfinsupp` as a `Finsupp`.

Note that the elaborator has a lot of trouble with this definition - it is often necessary to
write `(Dfinsupp.toFinsupp f : ι →₀ M)` instead of `f.to_finsupp`, as for some unknown reason
write `(Dfinsupp.toFinsupp f : ι →₀ M)` instead of `f.toFinsupp`, as for some unknown reason
using dot notation or omitting the type ascription prevents the type being resolved correctly. -/
def Dfinsupp.toFinsupp (f : Π₀ _i : ι, M) : ι →₀ M :=
⟨f.support, f, fun i => by simp only [Dfinsupp.mem_support_iff]⟩
Expand Down Expand Up @@ -234,7 +233,7 @@ def finsuppEquivDfinsupp [DecidableEq ι] [Zero M] [∀ m : M, Decidable (m ≠
#align finsupp_equiv_dfinsupp finsuppEquivDfinsupp

/-- The additive version of `finsupp.toFinsupp`. Note that this is `noncomputable` because
`Finsupp.hasAdd` is noncomputable. -/
`Finsupp.add` is noncomputable. -/
@[simps (config := { fullyApplied := false })]
def finsuppAddEquivDfinsupp [DecidableEq ι] [AddZeroClass M] [∀ m : M, Decidable (m ≠ 0)] :
(ι →₀ M) ≃+ Π₀ _i : ι, M :=
Expand All @@ -247,7 +246,7 @@ def finsuppAddEquivDfinsupp [DecidableEq ι] [AddZeroClass M] [∀ m : M, Decida
variable (R)

/-- The additive version of `Finsupp.toTinsupp`. Note that this is `noncomputable` because
`Finsupp.hasAdd` is noncomputable. -/
`Finsupp.add` is noncomputable. -/
-- porting note: `simps` generated lemmas that did not pass `simpNF` lints, manually added below
--@[simps? (config := { fullyApplied := false })]
def finsuppLequivDfinsupp [DecidableEq ι] [Semiring R] [AddCommMonoid M]
Expand Down Expand Up @@ -346,7 +345,7 @@ theorem sigmaFinsuppEquivDfinsupp_single [DecidableEq ι] [Zero N] (a : Σi, η
#align sigma_finsupp_equiv_dfinsupp_single sigmaFinsuppEquivDfinsupp_single

-- Without this Lean fails to find the `AddZeroClass` instance on `Π₀ i, (η i →₀ N)`.
attribute [-instance] Finsupp.hasZero
attribute [-instance] Finsupp.zero

@[simp]
theorem sigmaFinsuppEquivDfinsupp_add [AddZeroClass N] (f g : (Σi, η i) →₀ N) :
Expand Down Expand Up @@ -386,7 +385,7 @@ def sigmaFinsuppLequivDfinsupp [AddCommMonoid N] [Module R N] :
-- porting notes: was
-- sigmaFinsuppAddEquivDfinsupp with map_smul' := sigmaFinsuppEquivDfinsupp_smul
-- but times out
{ sigmaFinsuppEquivDfinsupp with
{ sigmaFinsuppEquivDfinsupp with
toFun := sigmaFinsuppEquivDfinsupp
invFun := sigmaFinsuppEquivDfinsupp.symm
map_add' := sigmaFinsuppEquivDfinsupp_add
Expand Down
20 changes: 10 additions & 10 deletions Mathlib/Data/Int/Range.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,12 @@ theorem mem_range_iff {m n r : ℤ} : r ∈ range m n ↔ m ≤ r ∧ r < n := b

#align int.mem_range_iff Int.mem_range_iff

instance decidableLeLt (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
instance decidableLELT (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
Decidable (∀ r, m ≤ r → r < n → P r) :=
decidable_of_iff (∀ r ∈ range m n, P r) <| by simp only [mem_range_iff, and_imp]
#align int.decidable_le_lt Int.decidableLeLt
#align int.decidable_le_lt Int.decidableLELT

instance decidableLeLe (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
instance decidableLELE (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
Decidable (∀ r, m ≤ r → r ≤ n → P r) := by
-- Porting note: The previous code was:
-- decidable_of_iff (∀ r ∈ range m (n + 1), P r) <| by
Expand All @@ -55,16 +55,16 @@ instance decidableLeLe (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
. intro _; apply h
simp_all only [mem_range_iff, and_imp, lt_add_one_iff]
. simp_all only [mem_range_iff, and_imp, lt_add_one_iff]
#align int.decidable_le_le Int.decidableLeLe
#align int.decidable_le_le Int.decidableLELE

instance decidableLtLt (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
instance decidableLTLT (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
Decidable (∀ r, m < r → r < n → P r) :=
Int.decidableLeLt P _ _
#align int.decidable_lt_lt Int.decidableLtLt
Int.decidableLELT P _ _
#align int.decidable_lt_lt Int.decidableLTLT

instance decidableLtLe (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
instance decidableLTLE (P : Int → Prop) [DecidablePred P] (m n : ℤ) :
Decidable (∀ r, m < r → r ≤ n → P r) :=
Int.decidableLeLe P _ _
#align int.decidable_lt_le Int.decidableLtLe
Int.decidableLELE P _ _
#align int.decidable_lt_le Int.decidableLTLE

end Int
Loading