chore: restore the binder overrides for structures f... | leanprover-community/mathlib4

In Lean 3 we had a mechanism to override argument expicitness for structure fields. We lost it during the port, but it's back!

Let's go through the list of uses in Lean 3, and decide which ones to keep.

grep -R -E '^\(.* \[\] : ' plus some post-processing gives:

src/algebra/char_p/basic.lean

(cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x)

src/algebra/direct_limit.lean

(map_self [] : ∀ i x h, f i i h x = x)
(map_map [] : ∀ {i j k} hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x)

src/algebra/module/localized_module.lean

(map_units [] : ∀ (x : S), is_unit (algebra_map R (module.End R M') x))
(surj [] : ∀ y : M', ∃ (x : M × S), x.2 • y = f x.1)
(eq_iff_exists [] : ∀ {x₁ x₂}, f x₁ = f x₂ ↔ ∃ c : S, c • x₂ = c • x₁)

src/algebra/order/absolute_value.lean

(abv_nonneg [] : ∀ x, 0 ≤ f x)
(abv_eq_zero [] : ∀ {x}, f x = 0 ↔ x = 0)
(abv_add [] : ∀ x y, f (x + y) ≤ f x + f y)
(abv_mul [] : ∀ x y, f (x * y) = f x * f y)

src/algebraic_topology/fundamental_groupoid/simply_connected.lean

(equiv_unit [] : nonempty (fundamental_groupoid X ≌ discrete unit))

src/category_theory/bicategory/coherence_tactic.lean

(hom [] : f ⟶ g)

src/category_theory/concrete_category/basic.lean

(forget [] : C ⥤ Type w)

src/category_theory/concrete_category/unbundled_hom.lean

(hom_id [] : ∀ {α} (ia : c α), hom ia ia id)
(hom_comp [] : ∀ {α β γ} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : β → γ} {f : α → β}

src/category_theory/functor/fully_faithful.lean

(map_injective' [] : ∀ {X Y : C}, function.injective (@functor.map _ _ _ _ F X Y) . obviously)

src/category_theory/limits/shapes/biproducts.lean

(out [] : ∀ n, has_biproducts_of_shape (fin n) C)

src/category_theory/limits/shapes/reflexive.lean

(common_section [] : ∃ (s : B ⟶ A), s ≫ f = 𝟙 B ∧ s ≫ g = 𝟙 B)
(common_retraction [] : ∃ (s : B ⟶ A), f ≫ s = 𝟙 A ∧ g ≫ s = 𝟙 A)

src/category_theory/limits/shapes/split_coequalizer.lean

(splittable [] : ∃ {Z : C} (h : Y ⟶ Z), nonempty (is_split_coequalizer f g h))

src/category_theory/localization/predicate.lean

(iso [] : L ⋙ F' ≅ F)

src/category_theory/monad/basic.lean

(η' [] : 𝟭 _ ⟶ to_functor)
(μ' [] : to_functor ⋙ to_functor ⟶ to_functor)
(ε' [] : to_functor ⟶ 𝟭 _)
(δ' [] : to_functor ⟶ to_functor ⋙ to_functor)

src/category_theory/monoidal/coherence.lean

(hom [] : X ⟶ Y)

src/category_theory/monoidal/functorial.lean

(ε [] : 𝟙_ D ⟶ F (𝟙_ C))

src/category_theory/monoidal/rigid/basic.lean

(coevaluation [] : 𝟙_ C ⟶ X ⊗ Y)
(evaluation [] : Y ⊗ X ⟶ 𝟙_ C)

src/category_theory/noetherian.lean

(subobject_lt_well_founded [] : well_founded ((<) : subobject X → subobject X → Prop))

src/category_theory/preadditive/injective_resolution.lean

(out [] : nonempty (InjectiveResolution Z))

src/category_theory/preadditive/projective_resolution.lean

(out [] : nonempty (ProjectiveResolution Z))

src/category_theory/triangulated/pretriangulated.lean

(distinguished_triangles [] : set (triangle C))

src/combinatorics/quiver/basic.lean

(obj [] : V → W)

src/computability/primrec.lean

(prim [] : nat.primrec (λ n, encodable.encode (decode n)))

src/control/random.lean

(random [] : Π (g : Type) [random_gen g], rand_g g α)

src/data/countable/defs.lean

(exists_injective_nat [] : ∃ f : α → ℕ, injective f)

src/data/fin_enum.lean

(equiv [] : α ≃ fin card) #24100

src/data/fintype/basic.lean

(elems [] : finset α)

src/data/json.lean (note: now in core)

(of_json [] : json → exceptional α)

src/deprecated/group.lean (skip, these are gone)

(map_add [] : ∀ x y, f (x + y) = f x + f y)
(map_mul [] : ∀ x y, f (x * y) = f x * f y)
(map_zero [] : f 0 = 0)
(map_one [] : f 1 = 1)

src/deprecated/ring.lean (skip, these are gone)

(map_zero [] : f 0 = 0)
(map_one [] : f 1 = 1)
(map_add [] : ∀ {x y}, f (x + y) = f x + f y)
(map_mul [] : ∀ {x y}, f (x * y) = f x * f y)
(map_one [] : f 1 = 1)
(map_mul [] : ∀ {x y}, f (x * y) = f x * f y)
(map_add [] : ∀ {x y}, f (x + y) = f x + f y)

src/field_theory/splitting_field/is_splitting_field.lean

(splits [] : splits (algebra_map K L) f)
(adjoin_root_set [] : algebra.adjoin K (f.root_set L) = ⊤)

src/geometry/manifold/charted_space.lean

(mem_chart_source [] : ∀x, x ∈ (chart_at x).source)
(compatible [] : ∀{e e' : local_homeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ G)

src/group_theory/is_free_group.lean

(mul_equiv [] : free_group generators ≃* G)

src/group_theory/nilpotent.lean

(nilpotent [] : ∃ n : ℕ, upper_central_series G n = ⊤)

src/group_theory/specific_groups/cyclic.lean

(exists_generator [] : ∃ g : α, ∀ x, x ∈ add_subgroup.zmultiples g)
(exists_generator [] : ∃ g : α, ∀ x, x ∈ zpowers g)

src/group_theory/subgroup/basic.lean

(conj_mem [] : ∀ n, n ∈ H → ∀ g : A, g + n + -g ∈ H)

src/linear_algebra/free_module/basic.lean

(exists_basis [] : nonempty (Σ (I : Type v), basis I R M))

src/logic/encodable/basic.lean

(decode [] : ℕ → option α)

src/measure_theory/covering/besicovitch.lean

(no_satellite_config [] : ∃ (N : ℕ) (τ : ℝ), 1 < τ ∧ is_empty (besicovitch.satellite_config α N τ))

src/measure_theory/group/action.lean

(measure_preimage_vadd [] : ∀ (c : M) ⦃s : set α⦄, measurable_set s → μ ((λ x, c +ᵥ x) ⁻¹' s) = μ s)
(measure_preimage_smul [] : ∀ (c : M) ⦃s : set α⦄, measurable_set s → μ ((λ x, c • x) ⁻¹' s) = μ s)

src/order/filter/bases.lean

(out [] : ∃ s : set (set α), s.countable ∧ f = generate s)

src/ring_theory/artinian.lean

(well_founded_submodule_lt [] : well_founded ((<) : submodule R M → submodule R M → Prop))

src/ring_theory/integral_closure.lean

(algebra_map_injective [] : function.injective (algebra_map A B))

src/ring_theory/localization/basic.lean

(map_units [] : ∀ y : M, is_unit (algebra_map R S y))
(surj [] : ∀ z : S, ∃ x : R × M, z * algebra_map R S x.2 = algebra_map R S x.1)
(eq_iff_exists [] : ∀ {x y}, algebra_map R S x = algebra_map R S y ↔ ∃ c : M, ↑c * x = ↑c * y)

src/ring_theory/principal_ideal_domain.lean

(principal [] : ∃ a, S = span R {a})

src/ring_theory/valuation/valuation_ring.lean

(cond [] : ∀ a b : A, ∃ c : A, a * c = b ∨ b * c = a)

src/testing/slim_check/sampleable.lean

(sample [] : gen α)
(sample [] : ∀ {α}, gen α → gen (F α))
(sample [] : ∀ {α β}, gen α → gen β → gen (F α β))
(interp [] : proxy_repr → α . sampleable.mk_trivial_interp)
(sample [] : gen proxy_repr)

src/topology/algebra/group/basic.lean

(Z [] : filter G)

src/topology/bornology/basic.lean

(cobounded [] : filter α)
(le_cofinite [] : cobounded ≤ cofinite)

src/topology/connected.lean

(is_totally_separated_univ [] : is_totally_separated (univ : set α))

src/topology/fiber_bundle/basic.lean

(total_space_mk_inducing [] : ∀ (b : B), inducing (@total_space.mk B F E b))
(trivialization_atlas [] : set (trivialization F (π F E)))
(trivialization_at [] : B → trivialization F (π F E))
(mem_base_set_trivialization_at [] : ∀ b : B, b ∈ (trivialization_at b).base_set)
(trivialization_mem_atlas [] : ∀ b : B, trivialization_at b ∈ trivialization_atlas)

src/topology/homotopy/contractible.lean

(hequiv_unit [] : nonempty (X ≃ₕ unit))

src/topology/metric_space/isometric_smul.lean

(isometry_vadd [] : ∀ c : M, isometry ((+ᵥ) c : X → X)) #24100
(isometry_smul [] : ∀ c : M, isometry ((•) c : X → X)) #24100

src/topology/metric_space/polish.lean

(second_countable [] : second_countable_topology α) #24100

src/topology/order.lean

(eq_bot [] : t = ⊥) #24100

src/topology/order/lower_topology.lean

(topology_eq_lower_topology [] : t = generate_from {s | ∃ a, (Ici a)ᶜ = s}) #24100

src/topology/subset_properties.lean

(noncompact_univ [] : ¬is_compact (univ : set α))
(is_preirreducible_univ [] : is_preirreducible (univ : set α))
(to_nonempty [] : nonempty α)

src/topology/vector_bundle/basic.lean

(continuous_on_coord_change' [] : ∀ (e e' : trivialization F (π F E)) [mem_trivialization_atlas e]

chore: restore the binder overrides for structures from Lean 3

Description

Contributor guide

First steps

Research direction

Assessment