unused arguments

Stream: condensed mathematics

[Johan Commelin]

@Ben Toner helpfully worked on CI for LTE. As a result, here is a list of unused arguments (for now):

/- The `unused_arguments` linter reports: -/
/- UNUSED ARGUMENTS. -/


-- for_mathlib/Gordan.lean
#print missing /- argument 2: [_inst_2 : fintype α] -/

-- for_mathlib/kronecker.lean
#print matrix.kronecker_mul /- argument 14: [_inst_9 : decidable_eq n'] -/

-- for_mathlib/rational_cones.lean
#print extended_le_span /- argument 11: (hx : x ∉ l) -/

-- normed_spectral.lean
#print system_of_double_complexes.normed_spectral_conditions.of_le /- argument 8: [_inst_4 : fact (1 ≤ k')] (duplicate) -/

-- polyhedral_lattice/Hom.lean
#print polyhedral_lattice.HomZ_map_equiv /- argument 3: [_inst_2 : fact (r' ≤ 1)] -/

-- polyhedral_lattice/cech.lean
#print PolyhedralLattice.Cech_conerve /- argument 4: [_inst_1 : fact (polyhedral_lattice_hom.to_add_monoid_hom f).range.saturated] (duplicate) -/
#print PolyhedralLattice.Cech_augmentation_map /- argument 4: [_inst_1 : fact (polyhedral_lattice_hom.to_add_monoid_hom f).range.saturated] (duplicate) -/
#print PolyhedralLattice.augmented_Cech_conerve /- argument 4: [_inst_1 : fact (polyhedral_lattice_hom.to_add_monoid_hom f).range.saturated] (duplicate) -/
#print PolyhedralLattice.augmentation_map_equalizes /- argument 4: [_inst_1 : fact (polyhedral_lattice_hom.to_add_monoid_hom f).range.saturated] (duplicate) -/

-- polyhedral_lattice/finsupp.lean
#print finsupp.has_norm /- argument 3: [_inst_1 : fintype ι] -/
#print generates_norm.finsupp_generators /- argument 3: [_inst_1 : fintype ι], argument 6: [_inst_3 : fintype J] -/

-- polyhedral_lattice/quotient.lean
#print polyhedral_lattice.quotient_finite /- argument 4: [H : fact L.saturated] -/

-- prop_92/concrete.lean
#print partial_sum_geom /- argument 2: (hr : 0 ≤ r) -/
#print locally_constant.map_zero /- argument 3: [_inst_2 : compact_space X] -/
#print locally_constant.comap_map /- argument 7: [_inst_10 : topological_space Y] -/
#print locally_constant.norm_map_aut /- argument 4: [_inst_5 : t2_space Y], argument 5: [_inst_6 : totally_disconnected_space Y] -/

-- prop_92/prop_92.lean
#print CLCFP.T_inv_sub_Tinv /- argument 10: [_inst_4 : fact (r' ≤ 1)] -/

-- pseudo_normed_group/CLC.lean
#print CLC.T /- argument 4: [_inst_2 : fact (0 < r)] -/
#print CLCFP.Tinv /- argument 6: [_inst_1 : fact (0 < r')] -/
#print CLCFP.T_inv_eq /- argument 6: [_inst_1 : normed_with_aut r V] (duplicate), argument 7: [_inst_2 : fact (0 < r)] (duplicate) -/
#print CLCFP.T_inv_app /- argument 7: [_inst_2 : fact (0 < r)] (duplicate) -/

-- pseudo_normed_group/LC.lean
#print LC.T_inv /- argument 4: [_inst_2 : fact (0 < r)] -/
#print LCFP.Tinv /- argument 6: [_inst_1 : fact (0 < r')] -/
#print LCFP.T /- argument 7: [_inst_2 : fact (0 < r)] -/
#print breen_deligne.universal_map.norm_eval_LCFP_le /- argument 9: [_inst_1 : normed_with_aut r V], argument 10: [_inst_2 : fact (0 < r)] -/

-- pseudo_normed_group/Tinv.lean
#print SemiNormedGroup.equalizer.map_id /- argument 2: [_inst_1 : category_theory.category J] -/
#print CLCFPTinv₂ /- argument 5: [_inst_6 : fact (0 < r')] -/
#print CLCFPTinv₂.map_norm_noninc /- argument 12: [_inst_6 : fact (c₂ ≤ c)] -/
#print CLCFPTinv₂.res /- argument 14: [_inst_6 : fact (c₂ ≤ c₁)], argument 16: [_inst_8 : fact (c₄ ≤ c₃)] -/
#print breen_deligne.universal_map.norm_eval_CLCFPTinv_le /- argument 3: [_inst_1 : normed_with_aut r V] (duplicate), argument 4: [_inst_2 : fact (0 < r)] (duplicate) -/
#print breen_deligne.universal_map.eval_CLCFPTinv_norm_noninc /- argument 3: [_inst_1 : normed_with_aut r V] (duplicate), argument 4: [_inst_2 : fact (0 < r)] (duplicate) -/

-- pseudo_normed_group/profinitely_filtered.lean
#print profinitely_filtered_pseudo_normed_group.prod_pi_homeo_pi_prod /- argument 3: [_inst_1 : Π (i : ι), profinitely_filtered_pseudo_normed_group (M i)] (duplicate) -/

-- rescale/FiltrationPow.lean
#print Filtration_cast_eq /- argument 5: [_inst_1 : fact (0 < r')] -/

-- rescale/normed_group.lean
#print SemiNormedGroup.nnnorm_to_rescale /- argument 2: [_inst_1 : fact (0 < r)] -/
#print SemiNormedGroup.of_rescale /- argument 2: [_inst_1 : fact (0 < r)] (duplicate) -/
#print SemiNormedGroup.iso_rescale /- argument 2: [_inst_1 : fact (0 < r)] (duplicate) -/

-- rescale/polyhedral_lattice.lean
#print generates_norm.rescale_generators /- argument 3: [_inst_1 : polyhedral_lattice Λ], argument 5: [_inst_2 : fintype J] -/

-- statement.lean
#print first_target_stmt /- argument 5: [_inst_3 : fact (r < r')], argument 6: [_inst_4 : fact (r < 1)], argument 11: [_inst_7 : ∀ (i : ℕ), fact (0 < κ i)] -/

-- thm95/col_exact.lean
#print thm95.CLCFP' /- argument 2: [_inst_3 : fact (0 < r')], argument 3: [_inst_5 : fact (r' < 1)] -/
#print thm95.FLC_arrow_hom' /- argument 2: [_inst_3 : fact (0 < r')], argument 3: [_inst_5 : fact (r' < 1)] -/
#print thm95.col_complex_rescaled.move_pls2 /- argument 2: [_inst_3 : fact (0 < r')] -/
#print thm95.col_complex_rescaled.T_inv_sub_Tinv_f_succ /- argument 5: [_inst_4 : fact (r < r')] -/
#print thm95.col_exact'_aux1 /- argument 3: [_inst_1 : BD.suitable κ] -/
#print thm95.col_exact'_aux2 /- argument 3: [_inst_1 : BD.suitable κ] -/

-- thm95/constants/default.lean
#print thm95.universal_constants.b /- argument 6: [_inst_3 : fact (0 < r)], argument 7: [_inst_4 : fact (0 < r')], argument 8: [_inst_5 : fact (r < r')], argument 9: [_inst_6 : fact (r' ≤ 1)] -/
#print thm95.universal_constants.K₁_spec /- argument 6: [_inst_3 : fact (0 < r)], argument 7: [_inst_4 : fact (0 < r')], argument 8: [_inst_5 : fact (r < r')], argument 9: [_inst_6 : fact (r' ≤ 1)] -/
#print thm95.universal_constants.c₀_aux /- argument 6: [_inst_1 : breen_deligne.package.adept BD κ κ'], argument 7: [_inst_2 : BD.data.very_suitable r r' κ] -/

-- thm95/default.lean
#print thm95.IH /- argument 6: [_inst_4 : fact (r < 1)] -/

-- thm95/double_complex.lean
#print thm95.Cech_nerve /- argument 3: [_inst_5 : fact (r' ≤ 1)] -/
#print thm95.cosimplicial_system_of_complexes /- argument 8: [_inst_4 : fact (r < r')] -/

-- thm95/homotopy.lean
#print norm_NSH_h_le /- argument 20: [_inst_8 : fact (thm95.universal_constants.c₀ r r' BD κ κ' m Λ ≤ c)] -/
#print NSH_δ_res /- argument 5: [_inst_3 : fact (r < r')] -/
#print NSH_δ /- argument 13: [_inst_7 : breen_deligne.package.adept BD κ κ'] -/

-- thm95/pfpng_iso.lean
#print ProFiltPseuNormGrpWithTinv.Pow_mul_comm_obj_equiv /- argument 2: [_inst_1 : fact (0 < r')] -/
#print ProFiltPseuNormGrpWithTinv.Pow_rescale_aux /- argument 2: [_inst_1 : fact (0 < r')] -/

-- thm95/polyhedral_iso.lean
#print PolyhedralLattice.Hom_finsupp_equiv /- argument 3: [_inst_1 : fact (0 < N)] -/
#print PolyhedralLattice.Hom_cosimplicial_zero_iso_aux /- argument 3: [_inst_1 : fact (0 < N)] -/
#print PolyhedralLattice.Hom_sum /- argument 7: [_inst_3 : fact (r' ≤ 1)] -/

-- thm95/row_iso.lean
#print FiltrationPow_rescale_iso /- argument 3: [_inst_5 : fact (r' ≤ 1)] -/
#print thm95.eval_FP_mul /- argument 3: [_inst_4 : fact (0 < r')], argument 4: [_inst_6 : fact (r' ≤ 1)], argument 11: [_inst_7 : fact (0 < N)] -/
#print thm95.mul_complex_iso /- argument 10: [_inst_5 : fact (r < r')] -/
#print thm95.quux /- argument 3: [_inst_4 : fact (0 < r')], argument 4: [_inst_6 : fact (r' ≤ 1)], argument 6: [_inst_7 : fact (0 < N)] -/

[Johan Commelin]

(Of course, this is a recursive process: once we've fixed these, new arguments may have become unused.)